{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:06Z","timestamp":1750219806881,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T00:00:00Z","timestamp":1673308800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2023,1,10]]},"abstract":"<jats:p>Many techniques of automated verification target multithreaded programs, because subtle interactions between threads may trigger concurrency errors such as deadlocks and data races. However, techniques and tools involving systematic exploration of the whole space of possible thread interleavings do not scale to large software systems, despite various clever algorithmic optimizations. A viable approach is to use incremental verification techniques that, in each run, focus just on the recently modified code and the relatively small number of affected execution traces, and therefore can provide results (bug reports) very quickly.<\/jats:p>\n          <jats:p>In this paper we present a new algorithm for incremental verification of multithreaded programs based on the pairwise approach, whose key idea is systematic exploration of all possible thread interleavings just for specific relevant pairs of threads.<\/jats:p>\n          <jats:p>We implemented the algorithm with Java Pathfinder as the backend verification tool, and evaluated it on several multithreaded Java programs. Results show that our incremental algorithm (1) can find errors very fast, (2) greatly reduces time needed for complete safety verification, and (3) it can find the same errors as full verification of the whole state space.<\/jats:p>","DOI":"10.1145\/3573074.3573082","type":"journal-article","created":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T03:38:24Z","timestamp":1674013104000},"page":"27-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs"],"prefix":"10.1145","volume":"48","author":[{"given":"Pavel","family":"Par\u00edzek","sequence":"first","affiliation":[{"name":"Charles University, Prague, Czech Rep"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Filip","family":"Kliber","sequence":"additional","affiliation":[{"name":"Charles University, Prague, Czech Rep"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213853"},{"key":"e_1_2_1_2_1","volume-title":"Model Checking. MIT Press","author":"Clarke E.","year":"2000","unstructured":"E. Clarke , O. Grumberg , and D. Peled . 2000 . Model Checking. MIT Press , 2000 . E. Clarke, O. Grumberg, and D. Peled. 2000. Model Checking. MIT Press, 2000."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of CAV","author":"Conway C.L.","year":"2005","unstructured":"C.L. Conway , K.S. Namjoshi , D. Dams , and S.A. Edwards . 2005. Incremental Algorithms for Inter-procedural Analysis of Safety Properties . Proceedings of CAV 2005 , LNCS 3576. C.L. Conway, K.S. Namjoshi, D. Dams, and S.A. Edwards. 2005. Incremental Algorithms for Inter-procedural Analysis of Safety Properties. Proceedings of CAV 2005, LNCS 3576."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of SPIN","author":"Flanagan C.","year":"2003","unstructured":"C. Flanagan and S. Qadeer . 2003. Thread-Modular Model Checking . Proceedings of SPIN 2003 , LNCS 2648. C. Flanagan and S. Qadeer. 2003. Thread-Modular Model Checking. Proceedings of SPIN 2003, LNCS 2648."},{"key":"e_1_2_1_5_1","volume-title":"Dynamic Partial-Order Reduction for Model Checking Software. POPL","author":"Flanagan C.","year":"2005","unstructured":"C. Flanagan and P. Godefroid . 2005 . Dynamic Partial-Order Reduction for Model Checking Software. POPL 2005 , ACM. C. Flanagan and P. Godefroid. 2005. Dynamic Partial-Order Reduction for Model Checking Software. POPL 2005, ACM."},{"key":"e_1_2_1_6_1","first-page":"2004","article-title":"Heuristics for Model Checking Java Programs","author":"Groce A.","year":"2004","unstructured":"A. Groce and W. Visser . 2004 . Heuristics for Model Checking Java Programs . International Journal on Software Tools for Technology Transfer, 6(4) , Spring er, 2004 . A. Groce and W. Visser. 2004. Heuristics for Model Checking Java Programs. International Journal on Software Tools for Technology Transfer, 6(4), Springer, 2004.","journal-title":"International Journal on Software Tools for Technology Transfer, 6(4)"},{"key":"e_1_2_1_7_1","volume-title":"Conc-iSE: Incremental Symbolic Execution of Concurrent Software. ASE","author":"Guo S.","year":"2016","unstructured":"S. Guo , M. Kusano , and C. Wang . 2016 . Conc-iSE: Incremental Symbolic Execution of Concurrent Software. ASE 2016 , ACM. S. Guo, M. Kusano, and C. Wang. 2016. Conc-iSE: Incremental Symbolic Execution of Concurrent Software. ASE 2016, ACM."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368128"},{"key":"e_1_2_1_10_1","volume-title":"Reduction: A Method of Proving Properties of Parallel Programs. Communications of the ACM, 18(12)","author":"Lipton R.J.","year":"1975","unstructured":"R.J. Lipton . Reduction: A Method of Proving Properties of Parallel Programs. Communications of the ACM, 18(12) , 1975 , ACM. R.J. Lipton. Reduction: A Method of Proving Properties of Parallel Programs. Communications of the ACM, 18(12), 1975, ACM."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of PLDI","author":"Liu B.","year":"2018","unstructured":"B. Liu and J. Huang . 2018. D4: Fast Concurrency Debugging with Parallel Differential Analysis . Proceedings of PLDI 2018 , ACM. B. Liu and J. Huang. 2018. D4: Fast Concurrency Debugging with Parallel Differential Analysis. Proceedings of PLDI 2018, ACM."},{"key":"e_1_2_1_12_1","volume-title":"Iterative Context Bounding for Systematic Testing of Multithreaded Programs. PLDI","author":"Musuvathi M.","year":"2007","unstructured":"M. Musuvathi and S. Qadeer . 2007 . Iterative Context Bounding for Systematic Testing of Multithreaded Programs. PLDI 2007 , ACM. M. Musuvathi and S. Qadeer. 2007. Iterative Context Bounding for Systematic Testing of Multithreaded Programs. PLDI 2007, ACM."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of OSDI","author":"Musuvathi M.","year":"2008","unstructured":"M. Musuvathi , S. Qadeer , T. Ball , G. Basler , P.A. Nainar , and I. Neamtiu . 2008. Finding and Reproducing Heisenbugs in Concurrent Programs . In Proceedings of OSDI 2008 , USENIX. M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P.A. Nainar, and I. Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In Proceedings of OSDI 2008, USENIX."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of WCET","volume":"4","author":"Nemer F.","year":"2006","unstructured":"F. Nemer , H. Casse , P. Sainrat , J.P. Bahsoun , and M. De Michiel . 2006. PapaBench: A Free Real-Time Benchmark . Proceedings of WCET 2006 , OASIcs, volume 4 . F. Nemer, H. Casse, P. Sainrat, J.P. Bahsoun, and M. De Michiel. 2006. PapaBench: A Free Real-Time Benchmark. Proceedings of WCET 2006, OASIcs, volume 4."},{"key":"e_1_2_1_15_1","volume-title":"Department of Distributed and Dependable Systems","author":"Parizek P.","year":"2022","unstructured":"P. Parizek and F. Kliber . Incremental Verification of Multithreaded Programs by Checking Interleavings for Pairs of Threads. Technical report no. D3S-TR-2022-01 , Department of Distributed and Dependable Systems , Charles University , 2022 . P. Parizek and F. Kliber. Incremental Verification of Multithreaded Programs by Checking Interleavings for Pairs of Threads. Technical report no. D3S-TR-2022-01, Department of Distributed and Dependable Systems, Charles University, 2022."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of TACAS","author":"Qadeer S.","year":"2005","unstructured":"S. Qadeer and J. Rehof . 2005. Context-Bounded Model Checking of Concurrent Software . Proceedings of TACAS 2005 , LNCS 3440. S. Qadeer and J. Rehof. 2005. Context-Bounded Model Checking of Concurrent Software. Proceedings of TACAS 2005, LNCS 3440."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of ICSM","author":"Yang G.","year":"2009","unstructured":"G. Yang , M.B. Dwyer , and G. Rothermel . Regression Model Checking . Proceedings of ICSM 2009 , IEEE CS. G. Yang, M.B. Dwyer, and G. Rothermel. Regression Model Checking. Proceedings of ICSM 2009, IEEE CS."},{"key":"e_1_2_1_18_1","volume-title":"Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004","author":"Yang Y.","year":"2008","unstructured":"Y. Yang , X. Chen , and G. Gopalakrishnan . 2008 . Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004 , University of Utah , 2008. Y. Yang, X. Chen, and G. Gopalakrishnan. 2008. Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004, University of Utah, 2008."},{"key":"e_1_2_1_19_1","unstructured":"Concurrency Tool Comparison repository https:\/\/facwiki.cs.byu.edu\/vv-lab\/index.php\/ Concurrency\\_Tool\\_Comparison  Concurrency Tool Comparison repository https:\/\/facwiki.cs.byu.edu\/vv-lab\/index.php\/ Concurrency\\_Tool\\_Comparison"},{"key":"e_1_2_1_20_1","unstructured":"Java Pathfinder verification framework (JPF) https: \/\/github.com\/javapathfinder\/jpf-core\/wiki  Java Pathfinder verification framework (JPF) https: \/\/github.com\/javapathfinder\/jpf-core\/wiki"},{"key":"e_1_2_1_21_1","unstructured":"Parallel Java Benchmarks https:\/\/bitbucket.org\/psl-lab\/pjbench  Parallel Java Benchmarks https:\/\/bitbucket.org\/psl-lab\/pjbench"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573074.3573082","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573074.3573082","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:37Z","timestamp":1750178737000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573074.3573082"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,10]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,10]]}},"alternative-id":["10.1145\/3573074.3573082"],"URL":"https:\/\/doi.org\/10.1145\/3573074.3573082","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2023,1,10]]},"assertion":[{"value":"2023-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}