{"id":"W2901173357","doi":"10.1007/978-3-030-03592-1_2","title":"Executable Counterexamples in Software Model Checking","year":2018,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Software Testing and Debugging Techniques","field":"Computer Science","cited_by":7,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Waterloo","funders":"","keywords":"Executable; Computer science; Programming language; Counterexample; Model checking; Software; Software engineering; Operating system; Discrete mathematics","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.002630684,0.001659503,0.001177647,0.002189579,0.0009135206,0.002836218,0.002140779,0.002150294,0.003545359],"category_scores_gemma":[0.02549235,0.001441904,0.001281278,0.001777739,0.004162752,0.005894029,0.00296109,0.005188094,0.000580215],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001432056,"about_ca_system_score_gemma":0.001026226,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001159787,"about_ca_topic_score_gemma":0.001623708,"domain_scores_codex":[0.9945278,0.002398692,0.0002497892,0.0004925948,0.002069079,0.0002621253],"domain_scores_gemma":[0.9823703,0.01509696,0.0004061889,0.001413622,0.000598595,0.0001143785],"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.0003086546,0.0001273562,0.0008144935,0.0004893879,0.00006855233,0.0004495071,0.0005048503,0.06617974,0.002595589,0.822625,0.004262884,0.1015739],"study_design_scores_gemma":[0.00003388104,0.00003648658,0.0001315967,0.0001614679,0.00004962737,0.000208951,0.00004867334,0.2111758,0.004253052,0.7792665,0.004610335,0.00002351782],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.04899308,0.002487976,0.9246115,0.001235807,0.0003886119,0.00008993044,0.00008568432,0.001851862,0.02025564],"genre_scores_gemma":[0.718583,0.001288799,0.2686963,0.0004078439,0.0002273194,0.0002106348,0.0002813486,0.0009082747,0.009396323],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.003545359,"threshold_uncertainty_score":0.01391256,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03569626035372483,"score_gpt":0.2674783825539967,"score_spread":0.2317821222002719,"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."}}