{"id":"W2547679913","doi":"10.1145/2950290.2950330","title":"SMT-based verification of parameterized systems","year":2016,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":43,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"European Research Council; U.S. Department of Defense","keywords":"Parameterized complexity; Decidability; Computer science; Modulo; Satisfiability; Reduction (mathematics); Satisfiability modulo theories; Horn clause; Theoretical computer science; Model checking; Algorithm; Formal verification; Automated theorem proving; Boolean satisfiability problem; Invariant (physics); Programming language; Mathematics; Discrete mathematics; Prolog","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.0005384616,0.00006128988,0.0001062328,0.00007187345,0.00002132753,0.00002715976,0.0005156545,0.00004178545,0.00001334321],"category_scores_gemma":[0.0001588197,0.00003814689,0.00003304951,0.0002072087,0.00004413812,0.0003197952,0.00003079155,0.00001910699,0.00005945655],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002898627,"about_ca_system_score_gemma":0.00003708155,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001623805,"about_ca_topic_score_gemma":1.474524e-7,"domain_scores_codex":[0.9991405,0.0001327776,0.000249495,0.0001893142,0.0001791615,0.0001087274],"domain_scores_gemma":[0.9988506,0.000132182,0.0001490859,0.0007317771,0.000101097,0.00003527811],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00001581134,0.00004337544,0.0002706662,0.00003116225,0.00000607762,2.622347e-7,0.00003983212,0.00004465318,0.2977446,0.6387337,0.0001424169,0.06292734],"study_design_scores_gemma":[0.0008689754,0.0001856497,0.008179342,0.00008605856,0.000005472344,0.00000369751,0.00001258492,0.281268,0.7025265,0.001481451,0.005154857,0.0002274712],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01621732,0.00001663881,0.9810456,0.0002042355,0.0003816879,0.0001396957,0.000001459871,0.0001310848,0.001862259],"genre_scores_gemma":[0.5459704,0.00000203192,0.453829,0.00002148719,0.00000767892,0.00001940899,3.399209e-7,0.000002547064,0.0001471112],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6372523,"threshold_uncertainty_score":0.1555585,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03274884067065573,"score_gpt":0.2694360252140056,"score_spread":0.2366871845433499,"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."}}