{"id":"W1996228525","doi":"10.1016/j.jlap.2003.07.006","title":"The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML","year":2003,"lang":"en","type":"article","venue":"The Journal of Logic and Algebraic Programming","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":154,"is_retracted":false,"has_abstract":false,"ca_institutions":"Prevention of Organ Failure","funders":"","keywords":"Programming language; Computer science; Java Modeling Language; Java; Java annotation; Generics in Java; Java applet; Java API for XML-based RPC; Mathematical proof; Semantics (computer science); Real time Java; Proof assistant; Mathematics","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":[],"consensus_categories":[],"category_scores_codex":[0.004695318,0.0001875558,0.0002843172,0.00008161558,0.0004628125,0.0004835768,0.0008696632,0.00008045962,0.000001090105],"category_scores_gemma":[0.0003309576,0.00009325821,0.0001327576,0.0004825707,0.0002048941,0.0003400522,0.00007460338,0.0002748033,0.000003320098],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004171602,"about_ca_system_score_gemma":0.0001076599,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001318366,"about_ca_topic_score_gemma":0.00001872706,"domain_scores_codex":[0.9978895,0.0003651469,0.0007290572,0.0002091105,0.0003073462,0.0004999006],"domain_scores_gemma":[0.9982465,0.0004720845,0.0005792309,0.0003655829,0.0002456154,0.00009101653],"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.00004061763,0.0001212431,0.002416243,0.00003120828,0.00005621203,0.000009822442,0.001547426,0.00001123326,0.0001067251,0.3851786,0.0001967927,0.6102839],"study_design_scores_gemma":[0.003211908,0.002689189,0.004153909,0.0000862315,0.0001267163,0.001530312,0.003529005,0.002387081,0.0008801055,0.4454326,0.5352241,0.0007488718],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1255812,0.02279453,0.8356205,0.008777697,0.001819285,0.004095886,7.490834e-7,0.0002156172,0.001094634],"genre_scores_gemma":[0.9910818,0.0001998826,0.008265569,0.0001222011,0.00009273435,0.00006359004,9.034815e-7,0.00001122015,0.0001621089],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.8655006,"threshold_uncertainty_score":0.4663142,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03373960461384942,"score_gpt":0.2609795963231573,"score_spread":0.2272399917093079,"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."}}