{"id":"W2028045996","doi":"10.1007/s10009-007-0047-9","title":"A framework for counterexample generation and exploration","year":2007,"lang":"en","type":"article","venue":"International Journal on Software Tools for Technology Transfer","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":31,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Toronto","funders":"","keywords":"Counterexample; Debugging; Mathematical proof; Computer science; Property (philosophy); Programming language; Theoretical computer science; Model checking; Algorithm; Mathematics; 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.007221956,0.002641736,0.00219971,0.005403483,0.001654256,0.00443478,0.005382692,0.003497821,0.01229925],"category_scores_gemma":[0.0309269,0.002013406,0.003975407,0.002452897,0.00334076,0.0070217,0.006344877,0.003344011,0.003300165],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001119023,"about_ca_system_score_gemma":0.00298371,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003194144,"about_ca_topic_score_gemma":0.004197693,"domain_scores_codex":[0.9917156,0.002761932,0.000664214,0.001328633,0.002843817,0.0006858612],"domain_scores_gemma":[0.9821365,0.01117551,0.0007308769,0.003804428,0.001862226,0.0002903213],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0006283402,0.0004119608,0.001623773,0.001012734,0.0003311954,0.0009099279,0.000900668,0.09950972,0.01599873,0.3938804,0.0110978,0.4736947],"study_design_scores_gemma":[0.0001322176,0.00009981624,0.0001810296,0.0001792546,0.0001632041,0.0004881216,0.000115538,0.7315498,0.02178187,0.2244771,0.02073351,0.00009849401],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0006781009,0.00005515616,0.9947701,0.00006228685,0.00001864368,0.00007689663,0.0000487016,0.003738882,0.0005511079],"genre_scores_gemma":[0.03837121,0.00008751372,0.9592814,0.00007288423,0.0000270682,0.0002133709,0.000215672,0.0008373125,0.0008935346],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01229925,"threshold_uncertainty_score":0.04114503,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1044817341754693,"score_gpt":0.368031216693099,"score_spread":0.2635494825176297,"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."}}