{"id":"W2487387108","doi":"10.4018/978-1-60960-086-0.ch013","title":"Formal Analysis of Real-Time Systems","year":2011,"lang":"en","type":"book-chapter","venue":"IGI Global eBooks","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Computer science; Automated theorem proving; Parallelism (grammar); Gas meter prover; Formal methods; Theoretical computer science; State (computer science); Programming language; Mathematics; Parallel computing; Mathematical proof","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.0005737503,0.0003408761,0.0008122131,0.0003234757,0.00006297921,0.00007646329,0.001512224,0.0004104355,0.00002730486],"category_scores_gemma":[0.00001866533,0.0003311431,0.0004300674,0.0001297583,0.0001083362,0.0002292454,0.0004063739,0.000159815,0.0001729576],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001886354,"about_ca_system_score_gemma":0.0001392036,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0003357357,"about_ca_topic_score_gemma":0.00001011918,"domain_scores_codex":[0.9978061,0.0000573729,0.0007359014,0.0005246709,0.0005370073,0.0003388968],"domain_scores_gemma":[0.9971829,0.00003503552,0.0007920735,0.001598949,0.0002596574,0.00013137],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00001105075,0.000005894603,0.000007040731,0.00003614984,0.0006026978,0.000006945413,0.00008801224,0.00003253532,0.00003481893,0.9929756,0.0001592037,0.006040041],"study_design_scores_gemma":[0.0009775852,0.001086448,0.001850855,0.0008699275,0.00687181,0.000158261,0.00002120232,0.1481345,0.00115549,0.7968766,0.03828584,0.003711468],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"other","genre_gemma":"methods","genre_scores_codex":[0.00004618135,0.00009200921,0.1603063,0.000001769536,0.0004619015,0.0002348255,0.00008586027,0.0001630643,0.8386081],"genre_scores_gemma":[0.1097943,0.00005818942,0.5309241,0.0001541294,0.0004646478,0.00008764002,0.00004386572,0.0001289598,0.3583441],"genre_candidate":"other","genre_consensus":null,"teacher_disagreement_score":0.480264,"threshold_uncertainty_score":0.9999141,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03411807452634276,"score_gpt":0.2722459132803901,"score_spread":0.2381278387540473,"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."}}