{"id":"W2151629759","doi":"10.1109/sefm.2005.44","title":"Stuttering abstraction for model checking","year":2005,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":12,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Abstraction; Computer science; Abstraction model checking; Model checking; Set (abstract data type); Scalability; Theoretical computer science; Construct (python library); Operator (biology); Abstract interpretation; Programming language; Database","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.002867026,0.001021587,0.0009167303,0.001079166,0.000749605,0.001393468,0.001072053,0.000796358,0.002471153],"category_scores_gemma":[0.005490012,0.0007935173,0.0036358,0.001045338,0.003110586,0.003019588,0.002453348,0.002992321,0.0006186167],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001542765,"about_ca_system_score_gemma":0.001461678,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002226596,"about_ca_topic_score_gemma":0.001932928,"domain_scores_codex":[0.9973442,0.0010117,0.0002404036,0.0003745335,0.0008369274,0.0001923625],"domain_scores_gemma":[0.9966375,0.001919442,0.0002649915,0.0009034657,0.0002059646,0.00006864456],"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.00009032343,0.00002654944,0.0005836381,0.0002796199,0.00009830468,0.0002913864,0.0006544596,0.1041311,0.01043518,0.8578002,0.001128204,0.02448089],"study_design_scores_gemma":[0.00003437443,0.00007798416,0.0001523336,0.00009678795,0.00008873871,0.0001394494,0.00004794934,0.2756717,0.008975726,0.7013507,0.01332234,0.00004184862],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.005688253,0.0002383635,0.9910822,0.0001010168,0.00003510022,0.00003788266,0.00004809069,0.001009231,0.001759896],"genre_scores_gemma":[0.370339,0.000972909,0.6233989,0.0003069711,0.0001304023,0.0004772279,0.0004214299,0.0005154614,0.003437699],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.002867026,"threshold_uncertainty_score":0.01516247,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.07152038508651672,"score_gpt":0.3475660622076079,"score_spread":0.2760456771210912,"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."}}