{"id":"W2035868375","doi":"10.1016/j.scico.2014.10.008","title":"Model checking of concurrent programs with static analysis of field accesses","year":2014,"lang":"en","type":"article","venue":"Science of Computer Programming","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":4,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Waterloo","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Computer science; Thread (computing); Heap (data structure); Tree traversal; Partial order reduction; Programming language; Java; Static analysis; Model checking; Distributed computing","routes":{"ca_aff":true,"ca_fund":true,"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.004394053,0.001203749,0.001196936,0.001758725,0.001035126,0.002574543,0.00282184,0.001191652,0.002062446],"category_scores_gemma":[0.01743547,0.001128596,0.002085844,0.001129241,0.003488241,0.004648001,0.002386739,0.001725141,0.0002499026],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002043676,"about_ca_system_score_gemma":0.00447224,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.007945425,"about_ca_topic_score_gemma":0.01074712,"domain_scores_codex":[0.993839,0.002239797,0.0002847438,0.0007941881,0.002036385,0.0008059831],"domain_scores_gemma":[0.982464,0.01164556,0.00149085,0.002974074,0.001185569,0.0002399893],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.001919712,0.000484179,0.01243097,0.0005003397,0.0003249416,0.0006935236,0.0007264534,0.7383962,0.04638654,0.1293091,0.001361364,0.06746671],"study_design_scores_gemma":[0.0001101113,0.0001170364,0.0003622748,0.00002736166,0.0001044381,0.00007479023,0.0000418731,0.9186908,0.02641952,0.05347002,0.0005531079,0.00002854947],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.2459838,0.0002094061,0.745102,0.000267203,0.00007737762,0.0001118498,0.0001781297,0.005590954,0.00247925],"genre_scores_gemma":[0.9483901,0.0000731634,0.05016825,0.00005905006,0.00002873926,0.00006699511,0.0001057206,0.0002156952,0.0008923184],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007945425,"threshold_uncertainty_score":0.02323824,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04364811075380737,"score_gpt":0.3294716491577327,"score_spread":0.2858235384039253,"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."}}