{"id":"W3048371688","doi":"10.1007/978-3-030-57663-9_1","title":"Teaching Formal Methods: An Experience Report","year":2020,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":7,"is_retracted":false,"has_abstract":false,"ca_institutions":"McMaster University","funders":"","keywords":"Computer science; Formal methods; Formal specification; Software engineering; Formal verification; Notation; Software deployment; Unified Modeling Language; Programming language; B-Method; Software","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","open_science"],"consensus_categories":[],"category_scores_codex":[0.004871063,0.0006659186,0.000681039,0.000682367,0.0005711991,0.0008127529,0.006439967,0.0004006173,0.00001576709],"category_scores_gemma":[0.0008287287,0.0006341073,0.0001635301,0.0006383812,0.0007741241,0.003998744,0.00250176,0.001744778,0.0000338489],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003661324,"about_ca_system_score_gemma":0.0005766746,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00004522872,"about_ca_topic_score_gemma":0.00001097755,"domain_scores_codex":[0.9939525,0.0002563866,0.001035452,0.002545271,0.0013226,0.000887798],"domain_scores_gemma":[0.9953116,0.0004056554,0.0006867147,0.00294641,0.0002428126,0.000406874],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000005032163,0.00001903594,0.00001169321,0.00002582874,0.000004942206,0.0002285266,0.003949931,0.0021671,0.0006760973,0.1316273,0.00000322002,0.8612813],"study_design_scores_gemma":[0.000139521,0.0002850647,0.00007081428,0.0001579248,0.000007329497,0.0008272764,0.00000145956,0.8412815,0.006516973,0.1426888,0.007091067,0.0009322336],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00005195665,0.0001354793,0.9868846,0.0005091635,0.002823427,0.0004379741,0.000001903618,0.0004574771,0.008698035],"genre_scores_gemma":[0.009991173,0.000008091546,0.9873596,0.001737396,0.000624218,0.00002368689,0.000006755644,0.00004525204,0.0002037724],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.860349,"threshold_uncertainty_score":0.999611,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05202268614598549,"score_gpt":0.3615113901187566,"score_spread":0.3094887039727711,"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."}}