{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,3]],"date-time":"2023-02-03T21:31:08Z","timestamp":1675459868559},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2019,2,2]],"date-time":"2019-02-02T00:00:00Z","timestamp":1549065600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.1007\/s10009-019-00507-5","type":"journal-article","created":{"date-parts":[[2019,2,2]],"date-time":"2019-02-02T04:58:51Z","timestamp":1549083531000},"page":"545-565","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Combining sequentialization-based verification of multi-threaded C programs with symbolic Partial Order Reduction"],"prefix":"10.1007","volume":"21","author":[{"given":"Vladimir","family":"Herdt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hoang M.","family":"Le","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Gro\u00dfe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,2,2]]},"reference":[{"key":"507_CR1","first-page":"141","volume-title":"Partial Orders for Efficient Bounded Model Checking of Concurrent Software","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial Orders for Efficient Bounded Model Checking of Concurrent Software, pp. 141\u2013157. Springer, Berlin (2013)"},{"key":"507_CR2","unstructured":"Andersen, L.O.: Program analysis and specialization for the C programming language. Dissertation, University of Copenhagen (1994)"},{"key":"507_CR3","first-page":"1","volume-title":"CONCUR 2004-Concurrency Theory","author":"T Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004-Concurrency Theory, pp. 1\u201315. Springer, Berlin (2004)"},{"key":"507_CR4","first-page":"331","volume-title":"Software Verification with Validation of Results","author":"D Beyer","year":"2017","unstructured":"Beyer, D.: Software Verification with Validation of Results, pp. 331\u2013349. Springer, Berlin (2017)"},{"key":"507_CR5","doi-asserted-by":"publisher","first-page":"61","DOI":"10.4204\/EPTCS.233.6","volume":"233","author":"D Beyer","year":"2016","unstructured":"Beyer, D., Friedberger, K.: A light-weight approach for verifying multi-threaded programs with CPAchecker. Electron. Proc. Theor. Comput. Sci. 233, 61\u201371 (2016)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"507_CR6","first-page":"184","volume-title":"CPAchecker: A Tool for Configurable Software Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M\u00a0.E.: CPAchecker: A Tool for Configurable Software Verification, pp. 184\u2013190. Springer, Berlin (2011)"},{"issue":"5","key":"507_CR7","first-page":"774","volume":"32","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking system C. TCAD 32(5), 774\u2013787 (2013)","journal-title":"TCAD"},{"key":"507_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). Lecture Notes in Computer Science, vol. 2988 , pp. 168\u2013176. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"507_CR9","doi-asserted-by":"crossref","unstructured":"Coons, K.E., Musuvathi, M., McKinley, K.S.: Bounded partial-order reduction. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA\u201913, pp. 833\u2013848. ACM, New York (2013)","DOI":"10.1145\/2509136.2509556"},{"key":"507_CR10","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B.: Verifying multi-threaded software using smt-based context-bounded model checking. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE \u201911, pp. 331\u2013340. ACM, New York (2011)","DOI":"10.1145\/1985793.1985839"},{"key":"507_CR11","first-page":"534","volume-title":"Context-Bounded Model Checking with ESBMC 1.17","author":"L Cordeiro","year":"2012","unstructured":"Cordeiro, L., Morse, J., Nicole, D., Fischer, B.: Context-Bounded Model Checking with ESBMC 1.17, pp. 534\u2013537. Springer, Berlin (2012)"},{"key":"507_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL\u201905, pp. 110\u2013121. ACM, New York (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"507_CR13","doi-asserted-by":"crossref","unstructured":"Ghafari, N., Hu, A.J., Rakamari\u0107, Z.: Context-bounded translations for concurrent software: an empirical evaluation. In: Proceedings of the 17th International SPIN Conference on Model Checking Software, SPIN\u201910, pp. 227\u2013244. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16164-3_17"},{"key":"507_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"P Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Secaucus (1996)"},{"key":"507_CR15","doi-asserted-by":"crossref","unstructured":"Hardekopf, B., Lin, C.: The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201907, pp. 290\u2013299. ACM, New York (2007)","DOI":"10.1145\/1250734.1250767"},{"key":"507_CR16","doi-asserted-by":"crossref","unstructured":"Herdt, V., Le, H., Gro\u00dfe, D., Drechsler, R.: Lazy-cseq-sp: boosting sequentialization-based verification of multi-threaded c programs via symbolic pruning of redundant schedules. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 9364, pp. 228\u2013233. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-24953-7_18"},{"key":"507_CR17","doi-asserted-by":"crossref","unstructured":"Inverso, O., Tomasco, E., Fischer, B., La\u00a0Torre, S., Parlato, G.: Bounded model checking of multi-threaded c programs via lazy sequentialization. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 8559, pp. 585\u2013602. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"507_CR18","volume-title":"Lazy-CSeq 0.6c: An Improved Lazy Sequentialization Tool for C","author":"O Inverso","year":"2014","unstructured":"Inverso, O., Tomasco, E., Fischer, B., Torre, S.L., Parlat, G.: Lazy-CSeq 0.6c: An Improved Lazy Sequentialization Tool for C. University of Southampton, Southampton (2014)"},{"key":"507_CR19","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In: Proceedings of the 21st International Conference on Computer Aided Verification, CAV \u201909, pp. 398\u2013413. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"507_CR20","doi-asserted-by":"crossref","unstructured":"La\u00a0Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 5643, pp. 477\u2013492. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_36"},{"issue":"1","key":"507_CR21","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. Form. Methods Syst. Des. 35(1), 73\u201397 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"507_CR22","doi-asserted-by":"crossref","unstructured":"Le, H.M., Gro\u00dfe, D., Herdt, V., Drechsler, R.: Verifying SystemC using an intermediate verification language and symbolic simulation. In: DAC, pp. 116:1\u2013116:6 (2013)","DOI":"10.1145\/2463209.2488877"},{"issue":"12","key":"507_CR23","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"507_CR24","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz. A.: Trace theory. In: Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency, pp. 279\u2013324. Springer, New York (1987)","DOI":"10.1007\/3-540-17906-2_30"},{"key":"507_CR25","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201907, pp. 446\u2013455. ACM, New York (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"507_CR26","unstructured":"Musuvathi, M., Qadeer, S.: Partial-order reduction for context-bounded state exploration. Technical Report MSR-TR-2007-12. Microsoft Research, Jan 2007"},{"key":"507_CR27","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3440, pp. 93\u2013107. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"507_CR28","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: Kiss: Keep it simple and sequential. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, PLDI \u201904, pp. 14\u201324. ACM, New York (2004)","DOI":"10.1145\/996841.996845"},{"key":"507_CR29","doi-asserted-by":"crossref","unstructured":"Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 489\u2013504. Springer, Berlin (2003)","DOI":"10.1007\/3-540-36577-X_36"},{"key":"507_CR30","doi-asserted-by":"crossref","unstructured":"Udupa, A., Desai, A., Rajamani, S.: Depth bounded explicit-state model checking. In: Groce, A., Musuvathi, M. (eds.) Model Checking Software. Lecture Notes in Computer Science, vol. 6823, pp. 57\u201374. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22306-8_5"},{"key":"507_CR31","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990, pp. 491\u2013515. Springer, Berlin (1991)"},{"key":"507_CR32","doi-asserted-by":"crossref","unstructured":"Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908\/ETAPS\u201908, pp. 382\u2013396. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_29"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00507-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00507-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00507-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,1]],"date-time":"2020-02-01T19:03:31Z","timestamp":1580583811000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00507-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,2]]},"references-count":32,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2019,10]]}},"alternative-id":["507"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00507-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2,2]]},"assertion":[{"value":"2 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}