{"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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001742501,0.0003136898,0.0003411023,0.0001839512,0.000099162,0.0002383026,0.002621322,0.0002783193,0.000008042275],"category_scores_gemma":[0.000351777,0.0002510568,0.0001251283,0.0002840265,0.00007801068,0.0002744459,0.002101998,0.0005588706,0.00005222817],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001826657,"about_ca_system_score_gemma":0.0003445598,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002830931,"about_ca_topic_score_gemma":0.000003192418,"domain_scores_codex":[0.9972973,0.0003322354,0.000438531,0.001181776,0.0003981991,0.0003519532],"domain_scores_gemma":[0.9966291,0.00002155556,0.0001715231,0.002803722,0.0002208446,0.0001533123],"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.0002153892,0.00241888,0.0005556549,0.005333782,0.0001137099,0.00000335047,0.02020319,0.02122431,0.003793649,0.5280057,0.001218852,0.4169135],"study_design_scores_gemma":[0.0001891943,0.0001788442,0.001112348,0.0002294795,0.00001709813,0.000004702702,0.00005089126,0.8485758,0.1329416,0.01295196,0.002719458,0.001028535],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.002329858,0.00005266986,0.9295954,0.0001549621,0.0006455258,0.001532925,0.00000151106,0.0005732014,0.06511397],"genre_scores_gemma":[0.1909403,6.282398e-7,0.8076519,0.0002455857,0.0000469972,0.0007658396,0.00000380826,0.00001671999,0.0003282365],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8273516,"threshold_uncertainty_score":0.9999942,"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."}}