{"id":"W2005214031","doi":"10.1145/2635868.2635911","title":"Verifying CTL-live properties of infinite state models using an SMT solver","year":2014,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Model checking; CTL*; Computer science; Solver; Satisfiability modulo theories; Computation tree logic; Liveness; Theoretical computer science; Abstraction; State (computer science); Abstraction model checking; Operator (biology); Abstract interpretation; Algorithm; Software; Programming language","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.000696909,0.00009856949,0.0001368733,0.00008715559,0.0000783685,0.00008012752,0.0005393749,0.00003291263,0.000005781658],"category_scores_gemma":[0.0000538489,0.00008018581,0.00002986843,0.0001735594,0.00006640559,0.001928581,0.0001748791,0.00007771014,0.000008541373],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002611866,"about_ca_system_score_gemma":0.00004405465,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002320286,"about_ca_topic_score_gemma":0.000005485903,"domain_scores_codex":[0.9989399,0.000155671,0.0002586911,0.0002342003,0.0002207806,0.0001907681],"domain_scores_gemma":[0.9990858,0.00002247543,0.0001262113,0.0005629606,0.0001473789,0.00005519453],"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.00005163607,0.0002124688,0.0003957033,0.0002208196,0.00003999213,0.000001119274,0.02382038,0.2903266,0.2396573,0.3145292,0.00002434102,0.1307203],"study_design_scores_gemma":[0.00008968915,0.00006225653,0.00008806807,0.00002732538,0.000002513442,0.000002030096,0.00005438105,0.8921596,0.1012838,0.006050245,0.00007160045,0.0001085256],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2860448,0.00001593333,0.7125314,0.00001247347,0.0001220609,0.00007664369,3.371653e-7,0.00007761876,0.001118699],"genre_scores_gemma":[0.5166429,0.000002808007,0.4831921,0.0001078069,0.00001131692,0.000002355389,1.924467e-7,0.000004969965,0.00003561547],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6018329,"threshold_uncertainty_score":0.3269883,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1584336444563301,"score_gpt":0.304024825010353,"score_spread":0.1455911805540229,"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."}}