{"id":"W2105167627","doi":"10.1145/1297666.1297670","title":"Automata-based assertion-checker synthesis of PSL properties","year":2008,"lang":"en","type":"article","venue":"ACM Transactions on Design Automation of Electronic Systems","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":94,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Assertion; Computer science; Programming language; Automaton; Debugging; Modular design; Operator (biology); Emulation; Set (abstract data type); Theoretical computer science; Büchi automaton; Deterministic automaton","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.001147592,0.0005409268,0.0004126763,0.0007950239,0.0004708291,0.001044255,0.0008995703,0.000457571,0.003585333],"category_scores_gemma":[0.00427346,0.0004537972,0.0008514694,0.0003072292,0.0008906989,0.001181253,0.0008135181,0.0008462645,0.001174245],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006042712,"about_ca_system_score_gemma":0.001467096,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001149869,"about_ca_topic_score_gemma":0.002103888,"domain_scores_codex":[0.998584,0.0003213707,0.0001705905,0.0002264693,0.000575147,0.0001223022],"domain_scores_gemma":[0.996443,0.001596129,0.0002658915,0.0008190143,0.0008061152,0.00006997865],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"bench_or_experimental","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000650636,0.0003356764,0.002905287,0.0008812744,0.0001598908,0.00125305,0.0007868744,0.2413764,0.2549719,0.2433281,0.008455951,0.2448951],"study_design_scores_gemma":[0.0001001596,0.0001743689,0.0002736724,0.00006066623,0.00008985293,0.0001857633,0.00004608906,0.7718745,0.1838554,0.03144341,0.01185884,0.00003726864],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02818723,0.00007516791,0.9589319,0.00008945398,0.00008259172,0.0001648664,0.0002462753,0.007231666,0.004990839],"genre_scores_gemma":[0.5176131,0.0001119069,0.4762763,0.0001295817,0.00003382767,0.0003859123,0.0007430075,0.000813948,0.003892403],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.003585333,"threshold_uncertainty_score":0.01199412,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06655507728057433,"score_gpt":0.2663195237633659,"score_spread":0.1997644464827915,"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."}}