{"id":"W4416099633","doi":"10.1007/978-3-032-10444-1_10","title":"A Rodin Plugin for Generating Proof Obligations for Invariant Preservation for ASTDs","year":2025,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":false,"ca_institutions":"Université de Sherbrooke","funders":"","keywords":"Plug-in; Correctness; JSON; Invariant (physics); Process calculus; Guard (computer science); Liveness; State (computer science)","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.002694373,0.0004225904,0.0004624044,0.0007792428,0.0006252856,0.0007054856,0.002673401,0.0003512109,0.00000178269],"category_scores_gemma":[0.001807894,0.0004179635,0.0001940105,0.0006347985,0.0002238667,0.001193984,0.0005611834,0.0003061616,0.000001008296],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003734597,"about_ca_system_score_gemma":0.001112123,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000008485015,"about_ca_topic_score_gemma":0.00005458405,"domain_scores_codex":[0.9966067,0.00004034676,0.0007659091,0.00148565,0.00049505,0.0006063083],"domain_scores_gemma":[0.9956091,0.001657777,0.000501116,0.001197879,0.000941207,0.00009293323],"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.00001799143,0.00002319724,0.000003774691,0.000258171,0.00001319439,3.403887e-7,0.0004352219,0.05565345,0.0007590605,0.485295,0.0002011578,0.4573394],"study_design_scores_gemma":[0.0003545277,0.0002372524,0.000006888773,0.000246613,0.00001241929,0.000002906402,1.355113e-7,0.7135593,0.008497598,0.2716852,0.005081037,0.0003160413],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00001071297,0.0001292065,0.9912571,0.00153298,0.002054421,0.004473495,0.00007274074,0.0001329921,0.0003363432],"genre_scores_gemma":[0.0009060104,0.000004405098,0.9953324,0.000975812,0.000616379,0.001156283,0.00006581368,0.00003070639,0.0009121423],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.6579059,"threshold_uncertainty_score":0.9998272,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05342179538499845,"score_gpt":0.3136844277840438,"score_spread":0.2602626323990453,"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."}}