{"id":"W1921908778","doi":"10.1109/icm.1998.825580","title":"Modeling and formal verification of a commercial microcontroller for embedded system applications","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":4,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Microcontroller; Correctness; Embedded system; Formal verification; Embedded software; Instruction set; Flowchart; Programming language; Abstraction; Assembly language; Software; Formal methods; Formal specification; Set (abstract data type); Software engineering; Computer architecture","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.00114202,0.0005943856,0.0002826737,0.000423456,0.0004210353,0.000961729,0.001079204,0.000804611,0.001979012],"category_scores_gemma":[0.003464158,0.0003570858,0.0006165484,0.0002571052,0.001258476,0.0009378551,0.0005228927,0.0008119998,0.0004030691],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001216836,"about_ca_system_score_gemma":0.001851716,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.005199816,"about_ca_topic_score_gemma":0.003976932,"domain_scores_codex":[0.9988213,0.0003499236,0.00007980097,0.0001399639,0.0005342683,0.00007470359],"domain_scores_gemma":[0.9985754,0.0008139201,0.0001351335,0.0002482842,0.0001980098,0.00002922356],"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.0001435968,0.0001511538,0.001553445,0.0004937028,0.00004664819,0.0007626577,0.0007138044,0.5768948,0.05153836,0.3192509,0.002013868,0.04643709],"study_design_scores_gemma":[0.00006435736,0.0001392048,0.0004290272,0.00007748867,0.0000478932,0.0002196891,0.00006633421,0.8918417,0.03417505,0.05339748,0.0195164,0.00002527764],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.04505431,0.0002626363,0.9476224,0.0003254795,0.00005148213,0.0002058865,0.0002273409,0.001410781,0.00483987],"genre_scores_gemma":[0.6088063,0.0005259594,0.3842446,0.00009418157,0.00003367551,0.0005835586,0.0006066163,0.0002409396,0.004864338],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.005199816,"threshold_uncertainty_score":0.01033908,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04174665769725585,"score_gpt":0.2760597214825729,"score_spread":0.234313063785317,"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."}}