{"id":"W1488842140","doi":"10.3233/sat190055","title":"QBF-Based Formal Verification: Experience and Perspectives","year":2008,"lang":"en","type":"article","venue":"Journal on Satisfiability Boolean Modeling and Computation","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":75,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Strong","keywords":"Formal methods; Formal verification; Computer science; 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.0008877631,0.0001508619,0.0001667707,0.0001403325,0.0007175994,0.0001944911,0.0002054593,0.00006314079,0.000002297846],"category_scores_gemma":[0.0001735859,0.0001408248,0.00004621952,0.0001803279,0.0001406128,0.001170504,0.00004958882,0.0002750095,0.000002768543],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00009449816,"about_ca_system_score_gemma":0.00008903855,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000008896621,"about_ca_topic_score_gemma":4.028245e-7,"domain_scores_codex":[0.9984233,0.0002144102,0.0003973008,0.0003891244,0.0003712502,0.0002046417],"domain_scores_gemma":[0.9990609,0.0001047021,0.0001778727,0.000259178,0.0002535041,0.0001438333],"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.0001534353,0.0002331565,0.00492361,0.00004849779,0.00001993852,0.00001308487,0.02499457,0.5683134,0.0003528818,0.05531229,0.00002847254,0.3456067],"study_design_scores_gemma":[0.0003744246,0.000214088,0.01743213,0.00002498206,0.000003628248,0.0001670556,0.0004571716,0.9750964,0.0001318192,0.005910355,0.00003150077,0.0001564301],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.4515346,0.00008968512,0.5478141,0.0002666392,0.00008484986,0.0000904674,4.420567e-7,0.00004955151,0.00006967276],"genre_scores_gemma":[0.694872,0.00006282615,0.3048845,0.0001124793,0.000047827,0.00001006398,8.253608e-7,0.000005398438,0.000004129336],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.406783,"threshold_uncertainty_score":0.5742668,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08181267425518404,"score_gpt":0.3148733832200596,"score_spread":0.2330607089648755,"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."}}