{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.004854208,0.001001105,0.000658936,0.001886273,0.001080041,0.002097355,0.002643913,0.0008316277,0.00466086],"category_scores_gemma":[0.008806346,0.0008380401,0.002723314,0.0008800619,0.003812929,0.002671883,0.002554987,0.002305384,0.001114023],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00134931,"about_ca_system_score_gemma":0.003106644,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002374551,"about_ca_topic_score_gemma":0.002001401,"domain_scores_codex":[0.9966738,0.0009163112,0.0003874258,0.0004480231,0.001292823,0.0002815407],"domain_scores_gemma":[0.9938053,0.003860303,0.000423674,0.001205956,0.0006015837,0.0001032588],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00007214292,0.0001783468,0.0009053365,0.0008038438,0.0001167231,0.0007509114,0.0006016743,0.1074283,0.01802749,0.7378618,0.003327678,0.1299256],"study_design_scores_gemma":[0.0001397372,0.0002677035,0.0004831741,0.0003384221,0.0001677251,0.0008566179,0.0001389626,0.4100261,0.03713815,0.4903102,0.06001556,0.000117606],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.000635169,0.0000352076,0.9979756,0.00005435873,0.0000144487,0.00004662861,0.00003857826,0.0006044214,0.0005956564],"genre_scores_gemma":[0.07791776,0.000286119,0.9188966,0.0001655393,0.00007023018,0.000337128,0.0002681569,0.0003090555,0.001749476],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.004854208,"threshold_uncertainty_score":0.02567178,"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."}}