{"id":"W2160243077","doi":"10.1016/j.entcs.2011.11.017","title":"Proving Reachability in B using Substitution Refinement","year":2011,"lang":"en","type":"article","venue":"Electronic Notes in Theoretical Computer Science","topic":"Security and Verification in Computing","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Sherbrooke","funders":"","keywords":"Reachability; Substitution (logic); Computer science; Statement (logic); State (computer science); Construct (python library); Property (philosophy); Programming language; Scheme (mathematics); Theoretical computer science; Mathematics; Law","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.003805073,0.0001644926,0.0001857232,0.0003560979,0.0002265942,0.000142225,0.001848679,0.00006493833,0.00001951436],"category_scores_gemma":[0.0002820556,0.0001596062,0.00004093794,0.001995528,0.001095008,0.0007215817,0.0006547209,0.0004280632,0.00000826317],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0007016531,"about_ca_system_score_gemma":0.0004800561,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001241375,"about_ca_topic_score_gemma":0.00003625635,"domain_scores_codex":[0.997122,0.000189552,0.0004605562,0.000878577,0.0004470848,0.0009021895],"domain_scores_gemma":[0.9987134,0.0002345543,0.00009354112,0.0007681078,0.00009384233,0.00009655248],"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.000007100958,0.0001602096,0.00236022,0.000007202504,9.286415e-7,0.00000557253,0.00130454,0.00066606,0.0004989157,0.971674,1.191613e-7,0.02331518],"study_design_scores_gemma":[0.0001889778,0.0001090006,0.006340201,0.00004557465,0.000001022287,0.00001815505,0.000004530921,0.7513274,0.007944617,0.2338304,0.00001172014,0.00017839],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.3548262,0.00004359534,0.6441636,0.0001153507,0.0002208642,0.000155078,8.821699e-8,0.00006706152,0.000408139],"genre_scores_gemma":[0.8408208,0.000003585978,0.159012,0.0001125199,0.0000386978,0.00000772343,2.315159e-7,0.000004097786,2.83447e-7],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.7506614,"threshold_uncertainty_score":0.6508552,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03090794954398939,"score_gpt":0.2734806031087783,"score_spread":0.2425726535647889,"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."}}