{"id":"W2125395260","doi":"10.1109/qsic.2007.4385519","title":"A Denotational Semantic Model for Validating JVML/CLDC Optimizations under Isabelle/HOL","year":2007,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université Laval; Concordia University","funders":"","keywords":"HOL; Computer science; Programming language; Concurrency; Denotational semantics; Semantics (computer science); Operational semantics; Extension (predicate logic); Theoretical computer science","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.001042845,0.0001058406,0.00009539408,0.0001264651,0.0002675152,0.000116816,0.0004766634,0.00005073084,0.00001765182],"category_scores_gemma":[0.0002116099,0.0001039836,0.00005519598,0.0003684626,0.00003080337,0.0006602961,0.00009818583,0.00006929514,0.00002421926],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00006130044,"about_ca_system_score_gemma":0.00008260564,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000004720063,"about_ca_topic_score_gemma":0.000008889546,"domain_scores_codex":[0.9988239,0.00003028056,0.0003237197,0.0002986804,0.0002431158,0.0002802719],"domain_scores_gemma":[0.9989316,0.0003016931,0.0001057382,0.0003688403,0.0002194928,0.0000726771],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000002587838,0.00003452583,0.00002469527,0.000008979059,0.000006961113,1.881076e-7,0.000398069,0.3327911,0.0007044793,0.662655,0.0002184432,0.00315497],"study_design_scores_gemma":[0.000219926,0.00001832159,0.0001438641,0.000006392912,0.000006438302,0.00000700868,0.00006866086,0.9647863,0.005043884,0.0295022,0.00006146401,0.0001355467],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.001485538,0.000009916012,0.9937283,0.0004217805,0.0001822448,0.0003177769,0.000002415083,0.0001954574,0.003656553],"genre_scores_gemma":[0.1389795,0.000001353785,0.8588743,0.0005303755,0.00003793147,0.00003139437,0.000009786315,0.0000110923,0.001524248],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.6331528,"threshold_uncertainty_score":0.4240328,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08547348748158205,"score_gpt":0.3600340148784934,"score_spread":0.2745605273969113,"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."}}