{"id":"W7020975202","doi":"","title":"Modular Verification of Distributed Systems with Grove","year":2022,"lang":"en","type":"dissertation","venue":"DSpace@MIT (Massachusetts Institute of Technology)","topic":"Distributed systems and fault tolerance","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Artificial Intelligence in Medicine (Canada)","funders":"","keywords":"Correctness; Modular design; Server; Key (lock); Formal verification; Mathematical proof; Lock (firearm); Formal specification","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.0003359836,0.0006137044,0.001272995,0.00100191,0.000241268,0.00008584852,0.002907766,0.0008664922,0.00001333055],"category_scores_gemma":[0.0001285475,0.0005855787,0.0002147758,0.002814313,0.0002882002,0.0006118725,0.0002318967,0.0008465184,0.000008902693],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002729475,"about_ca_system_score_gemma":0.0005056173,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002643548,"about_ca_topic_score_gemma":0.0001017813,"domain_scores_codex":[0.9961122,0.00006936221,0.001131989,0.001090746,0.001064368,0.000531302],"domain_scores_gemma":[0.9946675,0.00002629573,0.002049884,0.00246978,0.0006862585,0.0001002859],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"not_applicable","study_design_scores_codex":[0.0007382011,0.002726716,0.004909188,0.008683071,0.00403756,0.0006430621,0.003419115,0.03980392,0.04851626,0.8281192,0.01245286,0.04595087],"study_design_scores_gemma":[0.004411259,0.001964882,0.006873761,0.003678499,0.0006209571,0.0002151386,0.004180432,0.0291023,0.02591272,0.001542006,0.9180692,0.003428798],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.4063141,0.01832868,0.5281298,0.002961424,0.01501879,0.006412426,0.00888176,0.003248625,0.01070447],"genre_scores_gemma":[0.9896073,0.0001345201,0.005619607,0.000008934874,0.00004336101,0.0004138341,0.003017894,0.00005732894,0.001097258],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9056164,"threshold_uncertainty_score":0.9996595,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0077531021380128,"score_gpt":0.2301703827110786,"score_spread":0.2224172805730658,"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."}}