{"id":"W2996703997","doi":"10.1145/3371113","title":"The future is ours: prophecy variables in separation logic","year":2019,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Distributed systems and fault tolerance","field":"Computer Science","cited_by":60,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"Horizon 2020; Horizon 2020 Framework Programme; Fonds Wetenschappelijk Onderzoek; European Commission","keywords":"Separation logic; Computer science; Hoare logic; Correctness; Axiomatic semantics; Soundness; Programming language; Atomicity; Concurrency; Theoretical computer science; Operational semantics; Semantics (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.0006008554,0.0001386919,0.0001656949,0.00004122807,0.0001273302,0.0003297536,0.002646454,0.00007805917,0.000002533105],"category_scores_gemma":[0.0002035294,0.00007238064,0.00007337581,0.0005487605,0.0000383505,0.0003061218,0.0004409179,0.0001899454,0.0000164028],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003427782,"about_ca_system_score_gemma":0.00002657851,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002501833,"about_ca_topic_score_gemma":0.000005489262,"domain_scores_codex":[0.9988001,0.00001389087,0.0002443711,0.0003053274,0.0003498041,0.0002864871],"domain_scores_gemma":[0.99891,0.00005811604,0.000257587,0.0006020024,0.0001446215,0.00002769758],"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.00009455621,0.0004131252,0.06807125,0.0006086766,0.00009084085,0.000004223537,0.01096313,0.00006490204,0.01411421,0.5337126,0.01482601,0.3570365],"study_design_scores_gemma":[0.005106194,0.002259731,0.08775471,0.003874126,0.00008640006,0.0001500973,0.03316674,0.01277656,0.1225553,0.1057994,0.6238384,0.002632316],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9580981,0.002960375,0.0003740519,0.02886667,0.001163875,0.002132726,0.000008869103,0.0002675451,0.006127788],"genre_scores_gemma":[0.9918721,0.00002305767,0.006718586,0.0002518823,0.0001208964,0.00006519483,8.628038e-7,0.000009047913,0.0009383539],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.6090124,"threshold_uncertainty_score":0.4917815,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.00815648363780745,"score_gpt":0.2676606539177327,"score_spread":0.2595041702799252,"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."}}