{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T23:24:50Z","timestamp":1704842690098},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2011,11,1]],"date-time":"2011-11-01T00:00:00Z","timestamp":1320105600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2011,11]]},"abstract":"Abstract<\/jats:title>\n Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on the happens-before causality relations have been proposed for predictive analysis. However, these models often rely on only the observed runtime events and typically do not utilize the program source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted traces often suffer from the interleaving explosion problem. In this paper, we introduce a precise predictive model based on both the program source code and the observed execution events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events of the given trace. Rather than explicitly enumerating and checking the interleavings, our method conducts the search using a novel encoding and symbolic reasoning with a satisfiability modulo theory solver. We also propose a technique to bound the number of context switches allowed in the interleavings during the symbolic search, to further improve the scalability of the algorithm.<\/jats:p>","DOI":"10.1007\/s00165-011-0179-2","type":"journal-article","created":{"date-parts":[[2011,4,7]],"date-time":"2011-04-07T11:07:12Z","timestamp":1302174432000},"page":"781-805","source":"Crossref","is-referenced-by-count":10,"title":["Symbolic predictive analysis for concurrent programs"],"prefix":"10.1145","volume":"23","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[{"name":"NEC Laboratories America, Princeton, NJ, USA"}]},{"given":"Sudipta","family":"Kundu","sequence":"additional","affiliation":[{"name":"University of California, San Diego, CA, USA"}]},{"given":"Rhishikesh","family":"Limaye","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, CA, USA"}]},{"given":"Malay","family":"Ganai","sequence":"additional","affiliation":[{"name":"NEC Laboratories America, Princeton, NJ, USA"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"NEC Laboratories America, Princeton, NJ, USA"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Burckhardt S Alur R and Martin M (2007) CheckFence: checking consistency of concurrent data types on relaxed memory models. In: ACM SIGPLAN Conference on Programming Language Design and Implementation pp 12\u201321","DOI":"10.1145\/1273442.1250737"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Biere A Cimatti A Clarke E and Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and Algorithms for Construction and Analysis of Systems. LNCS vol 1579. Springer Berlin pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Beckman N Nori AV Rajamani SK Simmons RJ (2008) Proofs from tests. In: International Symposium on Software Testing and Analysis pp 3\u201314","DOI":"10.1145\/1390630.1390634"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Clarke E Kroening D Lerda F (2004) A tool for checking ANSI-C programs. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems. LNCS vol 2988. pp 168\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Chen F Rosu G (2007) Parametric and sliced causality. In: International Conference on Computer Aided Verification. LNCS vol 4590 Springer Berlin pp 240\u2013253","DOI":"10.1007\/978-3-540-73368-3_27"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Dutertre B and de Moura L (2006) A fast linear-arithmetic solver for DPLL(T). In International Conference on Computer Aided Verification. LNCS vol 4144. Springer Berlin pp 81\u201394","DOI":"10.1007\/11817963_11"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Freund SN (2004) Atomizer: a dynamic atomicity checker for multithreaded programs. In: Parallel and Distributed Processing Symposium","DOI":"10.1145\/964001.964023"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Freund SN Yi J (2008) Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation pp 293\u2013303","DOI":"10.1145\/1379022.1375618"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Godefroid P (2005) Dynamic partial-order reduction for model checking software. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages pp 110\u2013121","DOI":"10.1145\/1047659.1040315"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.84874"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Farzan A Madhusudan P (2006) Causal atomicity. In: International Conference on Computer Aided Verification. LNCS vol 4144. pp 315\u2013328","DOI":"10.1007\/11817963_30"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Farzan A Madhusudan P (2008) Monitoring atomicity in concurrent programs. In: International Conference on Computer Aided Verification. LNCS vol 5123. pp 52\u201365","DOI":"10.1007\/978-3-540-70545-1_8"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Farzan A Madhusudan P (2009) The complexity of predicting atomicity violations. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems pp 155\u2013169","DOI":"10.1007\/978-3-642-00768-2_14"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Farzan A Madhusudan P (2009) Meta-analysis for atomicity violations under nested locking. In: International Conference on Computer Aided Verification LNCS pp 248\u2013262","DOI":"10.1007\/978-3-642-02658-4_21"},{"key":"e_1_2_1_2_15_2","unstructured":"Farchi E Nir Y Ur S (2003) Concurrent bug patterns and how to test them. In: Parallel and Distributed Processing Symposium"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Qadeer S (2003) A type and effect system for atomicity. In: ACM SIGPLAN Conference on Programming Language Design and Implementation pp 338\u2013349","DOI":"10.1145\/780822.781169"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Havelund K Pressburger T (2000) Model checking Java programs using Java PathFinder. Softw Tools Technol Transf 2(4)","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_2_18_2","unstructured":"http:\/\/www2.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/index_1.html. The java grande forum benchmark suite."},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Ivan\u010di\u0107 F Yang Z Shlyakhter I Ganai MK Gupta A Ashar P (2005) F-Soft : Software verification platform. In: Computer-Aided Verification. LNCS vol 3576. Springer Berlin pp. 301\u2013306","DOI":"10.1007\/11513988_31"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0178-1"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Kahlon V Ivancic F Gupta A (2005) Reasoning about threads communicating via locks. In: International Conference on Computer Aided Verification. LNCS vol 3576. pp 505\u2013518","DOI":"10.1007\/11513988_49"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Kahlon V Wang C (2010) Universal Causality Graphs: a precise happens-before model for detecting bugs in concurrent programs. In: International Conference on Computer Aided Verification. LNCS vol 6174. Springer Berlin pp 434\u2013449","DOI":"10.1007\/978-3-642-14295-6_39"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Kahlon V Wang C Gupta A (2009) Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In: International Conference on Computer Aided Verification. pp 398\u2013413","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Lee J Padua D Midkiff S (1999) Basic compiler algorithms for parallel programs. In: Principles and Practice of Parallel Programming pp 1\u201312","DOI":"10.1145\/329366.301105"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Lahiri S Qadeer S (2008) Back to the future: revisiting precise program verification using SMT solvers. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages pp 171\u2013182","DOI":"10.1145\/1328897.1328461"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Lahiri S Qadeer S Rakamaric Z (2009) Static and precise detection of concurrency errors in systems code using SMT solvers. In: International Conference on Computer Aided Verification pp 509\u2013524","DOI":"10.1007\/978-3-642-02658-4_38"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Lal A Reps TW (2008) Reducing concurrent analysis under a context bound to sequential analysis. In: International Conference on Computer Aided Verification. LNCS vol 5123. pp 37\u201353","DOI":"10.1007\/978-3-540-70545-1_7"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Lu S Tucek J Qin F Zhou Y (2006) AVIO: detecting atomicity violations via access interleaving invariants. In: Architectural Support for Programming Languages and Operating Systems pp 37\u201348","DOI":"10.1145\/1168917.1168864"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Musuvathi M Qadeer S (2006) CHESS: systematic stress testing of concurrent software. In: Logic-Based Program Synthesis and Transformation. LNCS vol 4407. Springer Berlin pp 15\u201316","DOI":"10.1007\/978-3-540-71410-1_2"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Necula G McPeak S Rahul S and Weimer W (2002) CIL: Intermediate language and tools for analysis and transformation of c programs. In International Conference on Compiler Construction. LNCS 2304 pp. 213\u2013228","DOI":"10.1007\/3-540-45937-5_16"},{"key":"e_1_2_1_2_32_2","unstructured":"Qadeer S (2004) Joint CAV\/ISSTA special event on specification verification and testing of concurrent software"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Qadeer S Rehof J (2005) Context-bounded model checking of concurrent software. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems. Springer Berlin pp 93\u2013107","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Rabinovitz I Grumberg O (2005) Bounded model checking of concurrent programs. In: International Conference on Computer Aided Verification LNCS vol 2988. pp 82\u201397","DOI":"10.1007\/11513988_9"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_2_1_2_36_2","unstructured":"Serb\u0103nut\u0103 TF Chen F Rosu G (2008) Maximal causal models for multithreaded systems. Technical Report UIUCDCS-R-2008-3017 University of Illinois at Urbana-Champaign"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Sadowski C Freund SN Flanagan C (2009) Singletrack: a dynamic determinism checker for multithreaded programs. In: European Symposium on Programming pp 394\u2013409","DOI":"10.1007\/978-3-642-00590-9_28"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Sen K Rosu G Agha G (2005) Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Formal Methods for Open Object-Based Distributed Systems pp 211\u2013226","DOI":"10.1007\/11494881_14"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Said M Wang C Yang Z Sakallah K (2011) Generating data race witnesses by an SMT-based analysis. In: NASA Formal Methods Symposiumvon","DOI":"10.1007\/978-3-642-20398-5_23"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Praun C Gross TR (2004) Static detection of atomicity violations in object-oriented programs. Object Technol 3(6)","DOI":"10.5381\/jot.2004.3.6.a5"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Wang C Chaudhuri S Gupta A Yang Y (2009) Symbolic pruning of concurrent program executions. In: ACM SIGSOFT Symposium on Foundations of Software Engineering pp 23\u201332","DOI":"10.1145\/1595696.1595702"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Wang C Gupta A Ganai M (2006) Predicate learning and selective theory deduction for a difference logic solver. In: Design Automation Conference ACM New York pp 235\u2013240.","DOI":"10.1145\/1146909.1146971"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Wang C Ivan\u010di\u0107 F Ganai M Gupta A (2005) Deciding separation logic formulae by SAT and incremental negative cycle elimination. In: Logic for Programming Artificial Intelligence and Reasoning. LNCS vol 3835. Springer Berlin pp 322\u2013336","DOI":"10.1007\/11591191_23"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Wang C Kundu S Ganai M Gupta A (2009) Symbolic predictive analysis for concurrent programs. In: International Symposium on Formal Methods pp 256\u2013272","DOI":"10.1007\/978-3-642-05089-3_17"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Wang C Limaye R Ganai M Gupta A (2010) Trace-based symbolic analysis for atomicity violations. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems","DOI":"10.1007\/978-3-642-12002-2_27"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.1599419"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Wang C Said M Gupta A (2011) Coverage driven systematic concurrency testing. In: International Conference on Software Engineering","DOI":"10.1145\/1985793.1985824"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Wang C Yang Y Gupta A Gopalakrishnan G (2008) Dynamic model checking with property driven pruning to detect race conditions. In: Automated Technology for Verification and Analysis","DOI":"10.1007\/978-3-540-88387-6_11"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Wang C Yang Z Kahlon V Gupta A (2008) Peephole partial order reduction. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems pp 382\u2013396","DOI":"10.1007\/978-3-540-78800-3_29"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Xu M Bod\u00edk R Hill MD (2005) A serializability violation detector for shared-memory server programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation pp 1\u201314","DOI":"10.1145\/1064978.1065013"},{"key":"e_1_2_1_2_51_2","unstructured":"Yang Y Chen X Gopalakrishnan G (2008) Inspect: a runtime model checker for multithreaded C programs. Technical Report UUCS-08-004 University of Utah"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Yang Y Chen X Gopalakrishnan G Wang C (2009) Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis. In: SPIN workshop on Software Model Checking","DOI":"10.1007\/978-3-642-02652-2_22"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0179-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0179-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0179-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:59:36Z","timestamp":1641484776000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0179-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":52,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["10.1007\/s00165-011-0179-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0179-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11]]}}}