{"id":"W2017397762","doi":"10.5555/2818754.2818780","title":"Symbolic model checking of product-line requirements using SAT-based methods","year":2015,"lang":"en","type":"article","venue":"International Conference on Software Engineering","topic":"Advanced Software Engineering Methodologies","field":"Computer Science","cited_by":19,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Correctness; Model checking; Computer science; Feature (linguistics); Formal verification; Key (lock); Product (mathematics); Algorithm; Symbolic data analysis; Theoretical computer science; Programming language; Reliability engineering; 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.001625271,0.001504524,0.0009862399,0.001459329,0.0005978682,0.001746416,0.001871044,0.0009360416,0.00544965],"category_scores_gemma":[0.008729798,0.0009062189,0.002314118,0.001402835,0.001423245,0.002053661,0.001364795,0.001327062,0.0008684074],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001822045,"about_ca_system_score_gemma":0.002481773,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.009185717,"about_ca_topic_score_gemma":0.01396687,"domain_scores_codex":[0.997259,0.001176565,0.0001922861,0.0003360114,0.0008291985,0.0002069346],"domain_scores_gemma":[0.9913474,0.006613685,0.0004630583,0.0008867644,0.0006221357,0.00006707854],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000203848,0.0001031047,0.001570454,0.000389996,0.0001123306,0.0001729618,0.000170439,0.8958796,0.009511781,0.03297539,0.001331577,0.05757844],"study_design_scores_gemma":[0.00003102948,0.00002784007,0.00008885768,0.00001942583,0.00002066264,0.00002565966,0.00001464772,0.9866852,0.005343283,0.006926497,0.0008102023,0.000006672416],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01804057,0.00009193669,0.9759685,0.0000772458,0.00001682039,0.00008789651,0.0003280848,0.003428472,0.001960511],"genre_scores_gemma":[0.3897057,0.0002496839,0.605057,0.0001202004,0.00002612787,0.000428741,0.001685854,0.0006267758,0.002100089],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.009185717,"threshold_uncertainty_score":0.01826453,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.3360824296820287,"score_gpt":0.4339880477139365,"score_spread":0.09790561803190784,"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."}}