{"id":"W4315606532","doi":"10.1145/3571242","title":"Stratified Commutativity in Verification Algorithms for Concurrent Programs","year":2023,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":11,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Soundness; Commutative property; Algorithm; Computer science; Theoretical computer science; Abstraction; Programming language; Mathematics; Discrete 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.001177062,0.0001854526,0.0002553696,0.0001448613,0.0001430003,0.0002616881,0.002326185,0.00008976184,5.766811e-7],"category_scores_gemma":[0.000782813,0.0001306656,0.0001268716,0.001045253,0.0001036196,0.0002614638,0.0004833163,0.0001793378,0.000008403601],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004769667,"about_ca_system_score_gemma":0.00003461768,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00006932908,"about_ca_topic_score_gemma":0.00002076749,"domain_scores_codex":[0.9984026,0.00002470421,0.0003582684,0.0004186256,0.0003683074,0.0004274849],"domain_scores_gemma":[0.9987268,0.0001564484,0.0003264576,0.0005439572,0.0001921083,0.00005419005],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00001255697,0.0002567278,0.006033503,0.0003190574,0.00002574656,0.000001308862,0.004458415,0.000004319172,0.001684977,0.1727521,0.0003837732,0.8140675],"study_design_scores_gemma":[0.01180534,0.007659779,0.09663334,0.001250883,0.000217606,0.00008798114,0.03919343,0.05010536,0.2959791,0.3688973,0.1239021,0.004267857],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9476463,0.0009755882,0.02283281,0.009042428,0.002486589,0.01172164,0.0000142749,0.003034411,0.002245953],"genre_scores_gemma":[0.9842587,0.000007727811,0.01480087,0.00002724642,0.00006369574,0.0006237514,0.00001132651,0.00001699862,0.0001896778],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.8097997,"threshold_uncertainty_score":0.532839,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05947782296464332,"score_gpt":0.3218947002246022,"score_spread":0.2624168772599589,"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."}}