{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:47Z","timestamp":1753889747580,"version":"3.41.2"},"reference-count":67,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,8,5]],"date-time":"2012-08-05T00:00:00Z","timestamp":1344124800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In many practical application domains, the software is organized into a set\nof threads, whose activation is exclusive and controlled by a cooperative\nscheduling policy: threads execute, without any interruption, until they either\nterminate or yield the control explicitly to the scheduler. The formal\nverification of such software poses significant challenges. On the one side,\neach thread may have infinite state space, and might call for abstraction. On\nthe other side, the scheduling policy is often important for correctness, and\nan approach based on abstracting the scheduler may result in loss of precision\nand false positives. Unfortunately, the translation of the problem into a\npurely sequential software model checking problem turns out to be highly\ninefficient for the available technologies. We propose a software model\nchecking technique that exploits the intrinsic structure of these programs.\nEach thread is translated into a separate sequential program and explored\nsymbolically with lazy abstraction, while the overall verification is\norchestrated by the direct execution of the scheduler. The approach is\noptimized by filtering the exploration of the scheduler with the integration of\npartial-order reduction. The technique, called ESST (Explicit Scheduler,\nSymbolic Threads) has been implemented and experimentally evaluated on a\nsignificant set of benchmarks. The results demonstrate that ESST technique is\nway more effective than software model checking applied to the sequentialized\nprograms, and that partial-order reduction can lead to further performance\nimprovements.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:18)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":7,"title":["Software Model Checking with Explicit Scheduler and Symbolic Threads"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1315-6990","authenticated-orcid":false,"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Iman","family":"Narasamdya","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9483-3940","authenticated-orcid":false,"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,8,5]]},"reference":[{"issue":"2","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/fmsd\/AlurBHQR01","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1023\/A:1008767206905","volume":"18","author":"R. Alur, R. K. Brayton, T. A. Henzinger,","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/AndrewsQRRX04","doi-asserted-by":"crossref","unstructured":"T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In R. Alur and D. A. Peled, editors,CAV, volume 3114 ofLNCS, pages 484-487. Springer, 2004.","DOI":"10.1007\/978-3-540-27813-9_42"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/tacas\/BiereCCZ99","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. In R. Cleaveland, editor,TACAS, volume 1579 ofLNCS, pages 193-207. Springer, 1999.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"10.2168\/LMCS-8(2:18)2012_fmcad2009","doi-asserted-by":"crossref","unstructured":"D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software model checking via large-block encoding. InFMCAD, pages 25-32. IEEE, 2009.","DOI":"10.1109\/FMCAD.2009.5351147"},{"issue":"5-6","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/sttt\/BeyerHJM07","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer, T. A. Henzinger, R. Jhala, and","year":"2007","journal-title":"STTT"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/iccad\/BlancK08","doi-asserted-by":"crossref","unstructured":"N. Blanc and D. Kroening. Race analysis for SystemC using model checking. In S. R. Nassif and J. S. Roychowdhury, editors,ICCAD, pages 356-363. IEEE, 2008.","DOI":"10.1109\/ICCAD.2008.4681598"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/BeyerK11","doi-asserted-by":"crossref","unstructured":"D. Beyer and M. E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. In G. Gopalakrishnan and S. Qadeer, editors,CAV, volume 6806 ofLNCS, pages 184-190. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"10.2168\/LMCS-8(2:18)2012_Boussinot02","unstructured":"F. Boussinot.Operational Semantics of Cooperative Fair Threads, 2002. http:\/\/www-sop.inria.fr\/meije\/rp\/FairThreads\/FTC\/documentation\/semantics.pdf."},{"issue":"5","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/concurrency\/Boussinot06","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1002\/cpe.919","volume":"18","author":"F. Boussinot","year":"2006","journal-title":"Concurrency and Computation: Practice and Experience 18(5):445-469, 2006"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:series\/faia\/BarrettSST09","unstructured":"C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors,Handbook of Satisfiability, volume 185 ofFrontiers in Art. Int. and Applications, pages 825-885. IOS Press, 2009."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/fmcad\/CavadaCFKRS07","doi-asserted-by":"crossref","unstructured":"R. Cavada, A. Cimatti, A. Franz\u00e9n, K. Kalyanasundaram, M. Roveri, and R. K. Shyamasundar. Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. InFMCAD, pages 69-76. IEEE, 2007.","DOI":"10.1109\/FAMCAD.2007.35"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/spin\/CampanaCNR11","doi-asserted-by":"crossref","unstructured":"D. Campana, A. Cimatti, I. Narasamdya, and M. Roveri. An analytic evaluation of SystemC encodings in promela. In A. Groce and M. Musuvathi, editors,SPIN, volume 6823 ofLNCS, pages 90-107. Springer, 2011.","DOI":"10.1007\/978-3-642-22306-8_7"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/fmcad\/CimattiDJR09","doi-asserted-by":"crossref","unstructured":"A. Cimatti, J. Dubrovin, T. Junttila, and M. Roveri. Structure-aware computation of predicate abstraction. InFMCAD, pages 9-16. IEEE, 2009.","DOI":"10.1109\/FMCAD.2009.5351149"},{"issue":"4","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/toplas\/CytronFRWZ91","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron, J. Ferrante, B. K. Rosen, M.","year":"1991","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"5","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/jacm\/ClarkeGJLV03","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. M. Clarke, O. Grumberg, S. Jha, Y. Lu","year":"2003","journal-title":"J. ACM"},{"issue":"4","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/fac\/CimattiGMRTT98","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/s001650050022","volume":"10","author":"A. Cimatti, F. Giunchiglia, G. Mongardi,","year":"1998","journal-title":"Formal Asp. Comput."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/CimattiGMNR11","doi-asserted-by":"crossref","unstructured":"A. Cimatti, A. Griggio, A. Micheli, I. Narasamdya, and M. Roveri. Kratos - a software model checker for SystemC. In G. Gopalakrishnan and S. Qadeer, editors,CAV, volume 6806 ofLNCS, pages 310-316. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_24"},{"key":"10.2168\/LMCS-8(2:18)2012_ClarkeGrumbergPeledBook99","unstructured":"E. M. Clarke, O. Grumberg, and D. A. Peled.Model Checking. The MIT Press, 1999."},{"issue":"1","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/fmsd\/ClarkeJK07","first-page":"5","volume":"30","author":"E. M. Clarke, H. Jain, and D. Kroening","year":"2007","journal-title":"Formal Methods in System Design"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/tacas\/ClarkeKL04","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. Kroening, and F. Lerda. A Tool for Checking ANSI-C Programs. In K. Jensen and A. Podelski, editors,TACAS, volume 2988 ofLNCS, pages 168-176. Springer, 2004.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/tacas\/ClarkeKSY05","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. Kroening, N. Sharygina, and K. Yorav. SATABS: SAT-Based Predicate Abstraction for ANSI-C. In N. Halbwachs and L. D. Zuck, editors,TACAS, volume 3440 ofLNCS, pages 570-574. Springer, 2005.","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/fmcad\/CimattiMNR10","unstructured":"A. Cimatti, A. Micheli, I. Narasamdya, and M. Roveri. Verifying systemc: A software model checking approach. In R. Bloem and N. Sharygina, editors,FMCAD, pages 51-59. IEEE, 2010."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/tacas\/CimattiNR11","doi-asserted-by":"crossref","unstructured":"A. Cimatti, I. Narasamdya, and M. Roveri. Boosting lazy abstraction for systemc with partial order reduction. In P. A. Abdulla and K. R. M. Leino, editors,TACAS, volume 6605 ofLNCS, pages 341-356. Springer, 2011.","DOI":"10.1007\/978-3-642-19835-9_31"},{"issue":"3","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/entcs\/ChakiOYC03","first-page":"417","volume":"89","author":"S. Chaki, J. Ouaknine, K. Yorav, and E.","year":"2003","journal-title":"ENTCS"},{"key":"10.2168\/LMCS-8(2:18)2012_Craig:JSymLogic:1957","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/DonaldsonKKW11","doi-asserted-by":"crossref","unstructured":"A. F. Donaldson, A. Kaiser, D. Kroening, and T. Wahl. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In G. Gopalakrishnan and S. Qadeer, editors,CAV, volume 6806 ofLecture Notes in Computer Science, pages 356-371. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_28"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/popl\/EmmiQR11","doi-asserted-by":"crossref","unstructured":"M. Emmi, S. Qadeer, and Z. Rakamaric. Delay-bounded scheduling. In T. Ball and M. Sagiv, editors,POPL, pages 411-422. ACM, 2011.","DOI":"10.1145\/1925844.1926432"},{"key":"10.2168\/LMCS-8(2:18)2012_Floyd:AMS:1967","doi-asserted-by":"crossref","unstructured":"R. W. Floyd. Assigning meaning to programs. In J. T. Schwartz, editor,Proceedings of Symposium in Applied Mathematics, pages 19-32, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/spin\/FlanaganQ03","doi-asserted-by":"crossref","unstructured":"C. Flanagan and S. Qadeer. Thread-modular model checking. In T. Ball and S. K. Rajamani, editors,SPIN, volume 2648 ofLNCS, pages 213-224. Springer, 2003.","DOI":"10.1007\/3-540-44829-2_14"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/iscas\/GrosseD05","unstructured":"D. Gro\u00dfe and R. Drechsler. CheckSyC: an efficient property checker for RTL {SystemC designs}. InISCAS (4), pages 4167-4170. IEEE, 2005."},{"key":"10.2168\/LMCS-8(2:18)2012_GerstlauerEtAl:SystemDesign:01","unstructured":"A. Gerstlauer, R. Doemer, J. Peng, and D. D. Gajski.System Design: A Practical Guide with SpecC. Kluwer Academic Publishers, Boston, MA, USA, June 2001."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/spin\/GanaiG08","doi-asserted-by":"crossref","unstructured":"M. K. Ganai and A. Gupta. Efficient modeling of concurrent systems in BMC. In K. Havelund, R. Majumdar, and J. Palsberg, editors,SPIN, volume 5156 ofLNCS, pages 114-133. Springer, 2008.","DOI":"10.1007\/978-3-540-85114-1_10"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:books\/sp\/Godefroid96","doi-asserted-by":"crossref","unstructured":"P. Godefroid.Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 ofLNCS. Springer, 1996.","DOI":"10.1007\/3-540-60761-7"},{"issue":"2","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/fmsd\/Godefroid05","first-page":"77","volume":"26","author":"P. Godefroid","year":"2005","journal-title":"F. M. in Sys. Des."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/popl\/GuptaPR11","doi-asserted-by":"crossref","unstructured":"A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In T. Ball and M. Sagiv, editors,POPL, pages 331-344. ACM, 2011.","DOI":"10.1145\/1925844.1926424"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/GrafS97","doi-asserted-by":"crossref","unstructured":"Susanne Graf and Hassen Sa\u00efdi. Construction of abstract state graphs with pvs. In Orna Grumberg, editor,CAV, volume 1254 ofLNCS, pages 72-83. Springer, 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"issue":"4","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/sttt\/GroceV04","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/s10009-003-0130-9","volume":"6","author":"A. Groce and W. Visser","year":"2004","journal-title":"STTT"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/codes\/HerberFG08","doi-asserted-by":"crossref","unstructured":"P. Herber, J. Fellmuth, and S. Glesner. Model checking SystemC designs using timed automata. In C. H. Gebotys and G. Martin, editors,CODES+ISSS, pages 131-136. ACM, 2008.","DOI":"10.1145\/1450135.1450166"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/popl\/HenzingerJMM04","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In N. D. Jones and X. Leroy, editors,POPL, pages 232-244. ACM, 2004.","DOI":"10.1145\/964001.964021"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/HenzingerJMQ03","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer. Thread-modular abstraction refinement. In W. A. Hunt Jr. and F. Somenzi, editors,CAV, volume 2725 ofLNCS, pages 262-274. Springer, 2003.","DOI":"10.1007\/978-3-540-45069-6_27"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/popl\/HenzingerJMS02","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. InPOPL, pages 58-70. ACM, 2002.","DOI":"10.1145\/565816.503279"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/cacm\/Hoare83","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. An axiomatic basis for computer programming (reprint).Commun. ACM, 26(1):53-56, 1983.","DOI":"10.1145\/357980.358001"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/ac\/Holzmann05","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1016\/S0065-2458(05)65002-4","volume":"65","author":"G. J. Holzmann","year":"2005","journal-title":"Advances in Computers"},{"key":"10.2168\/LMCS-8(2:18)2012_HolzmannDoronFDT95","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann and D. A. Peled. An improvement in formal verification. In7th IFIP WG6.1 Int. Conf. on Formal Description Techniques VII, pages 197-211, London, UK, UK, 1995.","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"10.2168\/LMCS-8(2:18)2012_JohnsonBesnardGautierTalpin:AVoCS2010","unstructured":"K. Johnson, L. Besnard, T. Gautier, and J. P. Talpin. A synchronous approach to threaded program verification. InProc. of the 10th International Workshop on Automated Verification of Critical Systems, 2010."},{"issue":"4","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/toplas\/Jones83","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C. B. Jones","year":"1983","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/KahlonGS06","doi-asserted-by":"crossref","unstructured":"V. Kahlon, A. Gupta, and N. Sinha. Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In T. Ball and R. B. Jones, editors,CAV, volume 4144 ofLNCS, pages 286-299. Springer, 2006.","DOI":"10.1007\/11817963_28"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/memocode\/KroeningS05","unstructured":"D. Kroening and N. Sharygina. Formal verification of SystemC by automatic hardware\/software partitioning. InMEMOCODE, pages 101-110. IEEE, 2005."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/LahiriNO06","doi-asserted-by":"crossref","unstructured":"S. K. Lahiri, R. Nieuwenhuis, and A. Oliveras. SMT techniques for fast predicate abstraction. In T. Ball and R. B. Jones, editors,CAV, volume 4144 ofLNCS, pages 424-437. Springer, 2006.","DOI":"10.1007\/11817963_39"},{"issue":"1","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/fmsd\/LalR09","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A. Lal and T. W. Reps","year":"2009","journal-title":"Formal Methods in System Design"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/McMillan06","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Lazy abstraction with interpolants. In T. Ball and R. B. Jones, editors,CAV, volume 4144 ofLNCS, pages 123-136. Springer, 2006.","DOI":"10.1007\/11817963_14"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/acsd\/MoyMM05","unstructured":"M. Moy, F. Maraninchi, and L. Maillet-Contoz. Lussy: A toolbox for the analysis of systems-on-a-chip at the transactional level. InACSD, pages 26-35. IEEE, 2005."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/lopstr\/MusuvathiQ06","doi-asserted-by":"crossref","unstructured":"M. Musuvathi and S. Qadeer. Chess: Systematic stress testing of concurrent software. In G. Puebla, editor,LOPSTR, volume 4407 ofLNCS, pages 15-16. Springer, 2006.","DOI":"10.1007\/978-3-540-71410-1_2"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/pldi\/MusuvathiQ07","doi-asserted-by":"crossref","unstructured":"M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In J. Ferrante and K. S. McKinley, editors,PLDI, pages 446-455. ACM, 2007.","DOI":"10.1145\/1250734.1250785"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/acta\/OwickiG76","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. S. Owicki and D. Gries","year":"1976","journal-title":"Acta Inf."},{"key":"10.2168\/LMCS-8(2:18)2012_systemc","unstructured":"IEEE 1666: SystemC language Reference Manual, 2005. OSEK.OSEK\/VDX Operating System Specification 2.2.3, 2005. http:\/\/www.osek-vdx.org."},{"key":"10.2168\/LMCS-8(2:18)2012_PeledCAV93","doi-asserted-by":"crossref","unstructured":"D. A. Peled. All from one, one for all: on model checking using representatives. InCAV, volume 697 ofLNCS, pages 409-423. Springer, 1993.","DOI":"10.1007\/3-540-56922-7_34"},{"issue":"1","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/fmsd\/Peled96","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. A. Peled","year":"1996","journal-title":"Formal Methods in System Design"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/tacas\/QadeerR05","doi-asserted-by":"crossref","unstructured":"S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In N. Halbwachs and L. D. Zuck, editors,TACAS, volume 3440 ofLNCS, pages 93-107. Springer, 2005.","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/pldi\/QadeerW04","doi-asserted-by":"crossref","unstructured":"S. Qadeer and D. Wu. Kiss: keep it simple and sequential. In W. Pugh and C. Chambers, editors,PLDI, pages 14-24. ACM, 2004.","DOI":"10.1145\/996841.996845"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/RabinovitzG05","doi-asserted-by":"crossref","unstructured":"I. Rabinovitz and O. Grumberg. Bounded model checking of concurrent programs. In K. Etessami and S. K. Rajamani, editors,CAV, volume 3576 ofLNCS, pages 82-97. Springer, 2005.","DOI":"10.1007\/11513988_9"},{"key":"10.2168\/LMCS-8(2:18)2012_Schwoon2000","unstructured":"S. Schwoon.Model-Checking Pushdown Systems. PhD thesis, Lehrstuhl f\u00fcr informatik VII der Technischen Universit\u00e4t M\u00fcnchen, 2000."},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/spin\/TraulsenCMM07","doi-asserted-by":"crossref","unstructured":"C. Traulsen, J. Cornet, M. Moy, and F. Maraninchi. A SystemC\/TLM Semantics in Promela and Its Possible Applications. In D. Bosnacki and S. Edelkamp, editors,SPIN, volume 4595 ofLNCS, pages 204-222. Springer, 2007.","DOI":"10.1007\/978-3-540-73370-6_14"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/cav\/TorreMP09","doi-asserted-by":"crossref","unstructured":"S. L. Torre, P. Madhusudan, and G. Parlato. Reducing context-bounded concurrent reachability to sequential reachability. In A. Bouajjani and O. Maler, editors,CAV, volume 5643 ofLNCS, pages 477-492. Springer, 2009.","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"10.2168\/LMCS-8(2:18)2012_ValmariAPN90","doi-asserted-by":"crossref","unstructured":"A. Valmari. Stubborn sets for reduced state generation. InAPN 90: Proceedings on Advances in Petri nets 1990, pages 491-515, New York, NY, USA, 1991. Springer-Verlag.","DOI":"10.1007\/3-540-53863-1_36"},{"issue":"1","key":"10.2168\/LMCS-8(2:18)2012_DBLP:journals\/rts\/WaszniowskiH08","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L. Waszniowski and Z. Hanz\u00e1lek","year":"2008","journal-title":"Real-Time Systems"},{"key":"10.2168\/LMCS-8(2:18)2012_DBLP:conf\/tacas\/WangYKG08","doi-asserted-by":"crossref","unstructured":"C. Wang, Z. Yang, V. Kahlon, and A. Gupta. Peephole partial order reduction. In C. Ramakrishnan and J. Rehof, editors,TACAS, volume 4963 ofLNCS, pages 382-396. Springer, 2008.","DOI":"10.1007\/978-3-540-78800-3_29"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1032\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1032\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:01:42Z","timestamp":1681243302000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1032"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,5]]},"references-count":67,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:18)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1206.3182","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1206.3182","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-642-36742-7_7","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,8,5]]},"article-number":"1032"}}