{"id":"W3023134755","doi":"","title":"Hybrid verification integrating HOL theorem proving with MDG model checking","year":2006,"lang":"en","type":"article","venue":"Spectrum Research Repository (Concordia University)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Automated theorem proving; Computer science; Programming language; Model checking; Formal verification; Embedding; Theoretical computer science; Higher-order logic; Algorithm; Artificial intelligence; Description logic","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.001523852,0.0002079982,0.0002033113,0.0007084587,0.0009689075,0.0004843757,0.001603604,0.00008530127,0.000002640702],"category_scores_gemma":[0.0001142571,0.0002025395,0.00007909458,0.001297021,0.0003801928,0.001858173,0.0003763314,0.0007298476,0.00001436339],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0008018003,"about_ca_system_score_gemma":0.0005463355,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002845872,"about_ca_topic_score_gemma":0.0003349438,"domain_scores_codex":[0.9968561,0.0006029266,0.0002897246,0.0007812633,0.0007885731,0.0006813998],"domain_scores_gemma":[0.9980344,0.0001524586,0.0002134952,0.001082567,0.0003702492,0.0001468185],"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.0001142044,0.0001014237,0.01573517,0.00004705301,0.00002267703,0.0002236272,0.0003092816,0.003010831,0.0406327,0.9353747,0.0001099629,0.004318392],"study_design_scores_gemma":[0.0005424228,0.0003179349,0.01437448,0.00008891043,0.00001515708,0.0001055983,0.000397714,0.7261322,0.2461195,0.009641719,0.001795687,0.0004687034],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.3469318,0.00001736334,0.5722177,0.0001790531,0.0001080898,0.0003264859,0.00000113036,0.000241392,0.07997695],"genre_scores_gemma":[0.917927,0.000004653019,0.07911254,0.000006679321,0.000136318,0.000006510906,0.000004055355,0.00002229061,0.002779923],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.925733,"threshold_uncertainty_score":0.8259321,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03215153907610052,"score_gpt":0.2746139121595615,"score_spread":0.242462373083461,"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."}}