{"id":"W2117930267","doi":"10.1145/1086228.1086284","title":"Cutpoints for formal equivalence verification of embedded software","year":2005,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":31,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Formal equivalence checking; Equivalence (formal languages); Formal verification; Software; Program optimization; Theoretical computer science; Formal methods; Programming language; Computer engineering; Computer architecture; Mathematics; Discrete 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.005490378,0.001049034,0.000644898,0.00166628,0.0007059594,0.001838895,0.001906737,0.00111169,0.004988964],"category_scores_gemma":[0.01927309,0.0008030885,0.001682797,0.0008550032,0.003769403,0.003284305,0.002625027,0.003858733,0.0008480763],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001391984,"about_ca_system_score_gemma":0.001631515,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001597499,"about_ca_topic_score_gemma":0.0009991471,"domain_scores_codex":[0.9935638,0.002114725,0.000608372,0.0007848672,0.002585849,0.0003424829],"domain_scores_gemma":[0.9876305,0.009121248,0.0006243957,0.001477322,0.001026368,0.000120075],"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.0002102247,0.0001245341,0.0005817562,0.0007544289,0.0001019467,0.0004945552,0.0006015121,0.05730684,0.01917041,0.7881667,0.003318375,0.1291687],"study_design_scores_gemma":[0.0001758968,0.0001923667,0.0002288823,0.0002438206,0.00008063232,0.0003385372,0.0001051418,0.1780089,0.0491244,0.7458488,0.02558422,0.00006827414],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.002312797,0.0001155525,0.9955342,0.0000697659,0.00003415439,0.00008645342,0.00004422963,0.0009051081,0.0008976235],"genre_scores_gemma":[0.1839607,0.0005711433,0.811748,0.0002219429,0.00009948495,0.0007929506,0.0005042029,0.0005695513,0.001532099],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005490378,"threshold_uncertainty_score":0.02903622,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0377981304802072,"score_gpt":0.3222204679625033,"score_spread":0.2844223374822961,"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."}}