{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.007715617,0.001504675,0.001164791,0.001140072,0.001151014,0.002825747,0.003085553,0.001267138,0.001858571],"category_scores_gemma":[0.0259873,0.001681796,0.003690736,0.0008332983,0.005085489,0.007969614,0.003659499,0.002275483,0.0002691425],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002405443,"about_ca_system_score_gemma":0.003681784,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.005173127,"about_ca_topic_score_gemma":0.003930984,"domain_scores_codex":[0.9923269,0.00199082,0.0007215046,0.001739674,0.002530019,0.0006911363],"domain_scores_gemma":[0.9764308,0.01617059,0.00215803,0.003715119,0.001207748,0.0003176778],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0006442835,0.000284895,0.006106982,0.0008010014,0.000372682,0.001285066,0.001622825,0.6104596,0.05045706,0.2209927,0.0008567027,0.1061162],"study_design_scores_gemma":[0.0001517074,0.0001195254,0.0003916695,0.00006067871,0.0001231586,0.0001634157,0.00008194465,0.8727641,0.03505692,0.08862845,0.002409452,0.0000489778],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02205151,0.00004505688,0.9758125,0.00008631031,0.0000120797,0.0001075217,0.0000536143,0.001453321,0.0003780962],"genre_scores_gemma":[0.4614692,0.0001297482,0.5364597,0.0001119697,0.00003465236,0.0003478754,0.0002667684,0.0004386742,0.0007412712],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007715617,"threshold_uncertainty_score":0.04080456,"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."}}