{"id":"W2025670801","doi":"10.1145/1982185.1982531","title":"A proof-based approach to verifying reachability properties","year":2011,"lang":"en","type":"preprint","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Sherbrooke","funders":"","keywords":"Reachability; Temporal logic; Gas meter prover; Model checking; Computer science; Path (computing); Automated theorem proving; State (computer science); Property (philosophy); Operator (biology); Linear temporal logic; Proof theory; Sequence (biology); Theoretical computer science; Computation tree logic; Formal verification; Proof of concept; Algorithm; Programming language; Mathematics; Mathematical proof","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.005719187,0.001429934,0.001098661,0.00300988,0.001737454,0.003600998,0.003849091,0.002046301,0.008351184],"category_scores_gemma":[0.01763748,0.001116761,0.002590913,0.001361489,0.00316149,0.005228795,0.003276175,0.003494784,0.002758062],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001558799,"about_ca_system_score_gemma":0.002874527,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001705761,"about_ca_topic_score_gemma":0.001197762,"domain_scores_codex":[0.9932804,0.002615403,0.0005758096,0.0006954299,0.002515921,0.000317087],"domain_scores_gemma":[0.9876887,0.008840669,0.0004868124,0.001638615,0.001138085,0.0002070684],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0002599398,0.0003538447,0.0007831295,0.001786827,0.00026187,0.001128892,0.0007979063,0.0416483,0.04974921,0.6706814,0.005361272,0.2271874],"study_design_scores_gemma":[0.0003185482,0.0003393281,0.0003416257,0.0005029673,0.00020906,0.001590114,0.0001848327,0.2944792,0.08424154,0.5373946,0.08023696,0.0001612455],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0008220894,0.00008112899,0.9969612,0.0001193802,0.00003726625,0.00009680301,0.00004227981,0.0007168562,0.001122963],"genre_scores_gemma":[0.04817567,0.0003386564,0.9489648,0.0001969327,0.00004635884,0.000303605,0.0002065913,0.00031129,0.001456133],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.008351184,"threshold_uncertainty_score":0.03024632,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1844712782503363,"score_gpt":0.3028045220805012,"score_spread":0.1183332438301649,"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."}}