{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.00663899,0.001088198,0.000540035,0.001857326,0.001498539,0.00252972,0.001289014,0.001735804,0.03393173],"category_scores_gemma":[0.006625509,0.0005322671,0.000799438,0.001890586,0.0008198638,0.002642979,0.002688044,0.001650047,0.01185098],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001553899,"about_ca_system_score_gemma":0.003628514,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004807265,"about_ca_topic_score_gemma":0.006187733,"domain_scores_codex":[0.9954727,0.001451056,0.000169272,0.000427946,0.002003516,0.0004755769],"domain_scores_gemma":[0.9931273,0.001807206,0.0001140749,0.0005749733,0.002449085,0.001927181],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"not_applicable","study_design_scores_codex":[0.0003502121,0.005319149,0.003592207,0.0003499727,0.00002317433,0.0004881603,0.01035838,0.001214046,0.01012886,0.006694352,0.08474512,0.8767362],"study_design_scores_gemma":[0.0002058045,0.002416685,0.01004488,0.0004264857,0.00007754123,0.001869727,0.007634103,0.002960113,0.02598232,0.004540144,0.9437619,0.00008022139],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"other","genre_gemma":"empirical","genre_scores_codex":[0.2646416,0.01842906,0.1686051,0.008169329,0.002204693,0.001111757,0.002268538,0.008093616,0.5264764],"genre_scores_gemma":[0.286045,0.01317013,0.07054312,0.00111035,0.0003275252,0.0004776138,0.00387924,0.002424456,0.6220226],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.03393173,"threshold_uncertainty_score":0.1135129,"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."}}