{"id":"W1585202549","doi":"10.1007/978-3-540-69149-5_37","title":"Model-Checking Software Using Precise Abstractions","year":2008,"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":"University of Toronto","funders":"","keywords":"Computer science; Concurrency; Compiler; Software; Exploit; Software engineering; Software quality; Software construction; Software verification; Programming language; Software development; Software framework; Operating system; Distributed computing; Computer security","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.003163634,0.001598775,0.001267729,0.001133469,0.0006616423,0.001962367,0.002450208,0.001501533,0.00250466],"category_scores_gemma":[0.009040331,0.001986824,0.002342848,0.001118047,0.002722478,0.00544914,0.003235371,0.004544519,0.0006089584],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001017648,"about_ca_system_score_gemma":0.001347211,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001056372,"about_ca_topic_score_gemma":0.001496482,"domain_scores_codex":[0.9964679,0.0006840291,0.0002245857,0.0004499484,0.001908083,0.0002652922],"domain_scores_gemma":[0.994759,0.002530006,0.0002925672,0.002060993,0.0003030866,0.00005430303],"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.0001914778,0.00006321484,0.0008639221,0.0005581162,0.0001468845,0.0002928767,0.0006913948,0.2532372,0.02731112,0.5764749,0.002169909,0.137999],"study_design_scores_gemma":[0.00006907401,0.0001013463,0.0002389991,0.000131876,0.0001726156,0.0002328182,0.00005114102,0.4526346,0.04985181,0.4825387,0.01391824,0.00005874547],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00712478,0.000141496,0.9893364,0.00006652345,0.00004015015,0.00002939423,0.00002455575,0.001899942,0.001336718],"genre_scores_gemma":[0.3107992,0.0006565055,0.6808227,0.0001188097,0.00006512993,0.0001533647,0.0001848103,0.001083455,0.006115982],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.003163634,"threshold_uncertainty_score":0.01673108,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08131206888019911,"score_gpt":0.3120439415678036,"score_spread":0.2307318726876045,"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."}}