{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:35Z","timestamp":1725542975128},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642113185"},{"type":"electronic","value":"9783642113192"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11319-2_13","type":"book-chapter","created":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T05:00:05Z","timestamp":1262754005000},"page":"146-162","source":"Crossref","is-referenced-by-count":2,"title":["Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing"],"prefix":"10.1007","author":[{"given":"Jori","family":"Dubrovin","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"Compilers. Principles, Techniques, & Tools","author":"A.V. Aho","year":"2007","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers. Principles, Techniques, & Tools, 2nd edn. Addison-Wesley, Reading (2007)","edition":"2"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11817963_45","volume-title":"Computer Aided Verification","author":"S. Burckhardt","year":"2006","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: Bounded model checking of concurrent data types on relaxed memory models: a case study. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 489\u2013502. Springer, Heidelberg (2006)"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1250734.1250737","volume-title":"PLDI 2007","author":"S. Burckhardt","year":"2007","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: PLDI 2007, pp. 12\u201321. ACM, New York (2007)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/3-540-56863-8_47","volume-title":"Application and Theory of Petri Nets 1993","author":"S. Christensen","year":"1993","unstructured":"Christensen, S., Hansen, N.D.: Coloured Petri Nets extended with place capacities, test arcs and inhibitor arcs. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol.\u00a0691, pp. 186\u2013205. Springer, Heidelberg (1993)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"issue":"7","key":"13_CR7","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems\u00a027(7), 1165\u20131178 (2008)","journal-title":"IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Dubrovin, J.: Checking bounded reachability in asynchronous systems by symbolic event tracing. Tech. Rep. TKK-ICS-R14, Helsinki University of Technology, Department of Information and Computer Science (2009)","DOI":"10.1007\/978-3-642-11319-2_13"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-68863-1_7","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"J. Dubrovin","year":"2008","unstructured":"Dubrovin, J., Junttila, T., Heljanko, K.: Symbolic step encodings for object based communicating state machines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 96\u2013112. Springer, Heidelberg (2008)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science\u00a089(4) (2003)","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"13_CR11","volume-title":"Unfoldings \u2014 A Partial-Order Approach to Model Checking","author":"J. Esparza","year":"2008","unstructured":"Esparza, J., Heljanko, K.: Unfoldings \u2014 A Partial-Order Approach to Model Checking. Springer, Heidelberg (2008)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-85114-1_10","volume-title":"Model Checking Software","author":"M.K. Ganai","year":"2008","unstructured":"Ganai, M.K., Gupta, A.: Efficient modeling of concurrent systems in BMC. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 114\u2013133. Springer, Heidelberg (2008)"},{"issue":"1-2","key":"13_CR13","doi-asserted-by":"crossref","first-page":"91","DOI":"10.3233\/SAT190031","volume":"3","author":"M.K. Ganai","year":"2007","unstructured":"Ganai, M.K., Talupur, M., Gupta, A.: SDSAT: Tight integration of small domain encoding and lazy approaches in solving difference logic. Journal on Satisfiability, Boolean Modeling and Computation\u00a03(1-2), 91\u2013114 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1145\/1040305.1040316","volume-title":"POPL 2005","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided underapproximation-widening for multi-process systems. In: POPL 2005, pp. 122\u2013131. ACM, New York (2005)"},{"key":"13_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60794-3","volume-title":"Coloured Petri Nets. Basic Concepts, Analysis Methods, and Practical Use","author":"K. Jensen","year":"1997","unstructured":"Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods, and Practical Use, vol.\u00a01. Springer, Heidelberg (1997)"},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-004-0178-1","volume":"7","author":"T. Jussila","year":"2005","unstructured":"Jussila, T., Heljanko, K., Niemel\u00e4, I.: BMC via on-the-fly determinization. Int.\u00a0Journal on Software Tools for Technology Transfer\u00a07(2), 89\u2013101 (2005)","journal-title":"Int.\u00a0Journal on Software Tools for Technology Transfer"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-540-73368-3_5","volume-title":"Computer Aided Verification","author":"L.M. Moura de","year":"2007","unstructured":"de Moura, L.M., Dutertre, B., Shankar, N.: A tutorial on satisfiability modulo theories. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 20\u201336. Springer, Heidelberg (2007)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: Benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 82\u201397. Springer, Heidelberg (2005)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 209\u2013222. Springer, Heidelberg (2002)"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-78800-3_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Wang","year":"2008","unstructured":"Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 382\u2013396. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11319-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T12:28:57Z","timestamp":1590496137000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11319-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642113185","9783642113192"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11319-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}