{"id":"W4243742593","doi":"10.1145/2103656.2103693","title":"Verification of parameterized concurrent programs by modular reasoning about data and control","year":2012,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":30,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Thread (computing); Computer science; Parameterized complexity; Modular design; Programming language; Separation logic; Control flow; Theoretical computer science; Bounded function; Boolean data type; Model checking; Parallel computing; Algorithm; 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.001178237,0.00008899628,0.0001515993,0.00002856586,0.00004283563,0.00006597312,0.0007088784,0.00004666264,0.000003940584],"category_scores_gemma":[0.0001876717,0.00007726679,0.00001532832,0.0001432033,0.00007952173,0.001129184,0.0001793647,0.00006301074,0.000004647861],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001319471,"about_ca_system_score_gemma":0.00001377207,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001950331,"about_ca_topic_score_gemma":1.94002e-7,"domain_scores_codex":[0.9989355,0.0001527818,0.0002565848,0.0002649535,0.0001857793,0.0002044574],"domain_scores_gemma":[0.9986248,0.0000533393,0.0001783765,0.0009982322,0.00005706757,0.00008819323],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00001576604,0.0002223784,0.006621482,0.00005131949,0.00003499026,9.954273e-8,0.000610303,0.000002721199,0.07319242,0.135742,0.0002489964,0.7832575],"study_design_scores_gemma":[0.0009544386,0.0001185328,0.01271413,0.00003752712,0.00002561661,0.000009092489,0.00004734676,0.9425108,0.02910712,0.0002003916,0.01403686,0.0002381461],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.05435072,0.0008495423,0.9439613,0.00005490503,0.0002376101,0.0002899778,0.00001107738,0.00007782501,0.0001670051],"genre_scores_gemma":[0.5723208,0.00002612092,0.4275583,0.00002350511,0.00001273836,0.00001736123,0.00002676735,0.000003206605,0.00001113303],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9425081,"threshold_uncertainty_score":0.3150848,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05235170920159668,"score_gpt":0.3187935233458588,"score_spread":0.2664418141442622,"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."}}