{"id":"W2973427087","doi":"10.1109/access.2019.2942829","title":"A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving","year":2019,"lang":"en","type":"article","venue":"IEEE Access","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":11,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Computer science; Automated theorem proving; Formal verification; Probabilistic logic; Fault tree analysis; Theoretical computer science; Model checking; Spare part; Formal methods; Algorithm; Programming language; Reliability engineering; Artificial intelligence","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002082709,0.0001064439,0.0001760167,0.00009836319,0.0001247258,0.0001128718,0.001793234,0.00007711633,0.000003617113],"category_scores_gemma":[0.0002494575,0.00007604593,0.00007585924,0.0003289567,0.00007330282,0.001628822,0.0001556136,0.000098073,0.000003958932],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00005009749,"about_ca_system_score_gemma":0.0000693577,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00005649361,"about_ca_topic_score_gemma":0.00001121329,"domain_scores_codex":[0.9987533,0.0002464523,0.000304962,0.0002804655,0.0001735034,0.0002412841],"domain_scores_gemma":[0.9979189,0.0007522649,0.0003453611,0.0008038424,0.0001578878,0.00002174377],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000134738,0.00006510183,0.0009668743,0.0001977288,0.0000612567,2.949443e-7,0.002254272,0.01140951,0.2695946,0.2232135,0.00001986283,0.4920824],"study_design_scores_gemma":[0.0002398934,0.00006708514,0.006181119,0.00001788307,0.00001668376,0.000007279122,0.00007936816,0.8992696,0.08783071,0.0060481,0.0001351299,0.0001071708],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2678159,0.00004662988,0.73052,0.00007230738,0.0007947554,0.0005995712,0.000002899725,0.00003944565,0.0001085244],"genre_scores_gemma":[0.5806243,0.000004945567,0.4192277,0.0000457324,0.00002429943,0.00004347399,9.719249e-7,0.000007107837,0.00002142685],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.8878601,"threshold_uncertainty_score":0.3332305,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1409429394816265,"score_gpt":0.4142818508273672,"score_spread":0.2733389113457407,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}