{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,24]],"date-time":"2026-01-24T17:39:42Z","timestamp":1769276382861,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642221095","type":"print"},{"value":"9783642221101","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_55","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T13:08:45Z","timestamp":1309784925000},"page":"669-685","source":"Crossref","is-referenced-by-count":60,"title":["Practical, Low-Effort Equivalence Verification of Real Code"],"prefix":"10.1007","author":[{"given":"David A.","family":"Ramos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dawson R.","family":"Engler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"55_CR1","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Model checking programs. In: IEEE International Conference on Automated Software Engineering, ASE 2000 (2000)"},{"key":"55_CR2","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. of the Eighth Symposium on Operating Systems Design and Implementation (OSDI 2008), pp. 209\u2013224 (December 2008)"},{"key":"55_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11537328_2","volume-title":"Model Checking Software","author":"C. Cadar","year":"2005","unstructured":"Cadar, C., Engler, D.: Execution generated test cases: How to make systems code crash itself. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 2\u201323. Springer, Heidelberg (2005)"},{"key":"55_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: Proc. of the Asia and South Pacific Design Automation Conference, ASP-DAC 2003 (2003)","DOI":"10.1145\/1119772.1119831"},{"key":"55_CR5","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S.: Bandera: Extracting finite-state models from Java source code. In: Proc. of the 22nd International Conference on Software Engineering (ICSE 2000), pp. 439\u2013448 (June 2000)","DOI":"10.1145\/337180.337234"},{"key":"55_CR6","doi-asserted-by":"crossref","unstructured":"Deng, X., Lee, J.: Bogor\/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In: Proc. of the 21st IEEE International Conference on Automated Software Engineering, pp. 157\u2013166 (2006)","DOI":"10.1109\/ASE.2006.26"},{"key":"55_CR7","doi-asserted-by":"crossref","unstructured":"Elkarablieh, B., Marinov, D., Khurshid, S.: Efficient solving of structural constraints. In: Proc. of the International Symposium on Software Testing and Analysis, pp. 39\u201350 (2008)","DOI":"10.1145\/1390630.1390637"},{"key":"55_CR8","doi-asserted-by":"crossref","unstructured":"Engler, D., Dunbar, D.: Under-constrained execution: making automatic code destruction easy and scalable. In: Proc. of the International Symposium on Software Testing and Analysis, ISSTA (July 2007)","DOI":"10.1145\/1273463.1273464"},{"key":"55_CR9","doi-asserted-by":"crossref","unstructured":"Engler, D., Yu Chen, D., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: A general approach to inferring errors in systems code. In: Proc. of the 18th ACM Symposium on Operating Systems Principles, SOSP 2001 (2001)","DOI":"10.21236\/ADA419584"},{"key":"55_CR10","doi-asserted-by":"crossref","unstructured":"Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: Proc. of the 32nd International Conference on Software Engineering (ICSE 2010), pp. 225\u2013234 (2010)","DOI":"10.1145\/1806799.1806835"},{"key":"55_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proc. of the 24th Annual Symposium on Principles of Programming Languages (POPL 1997), pp. 174\u2013186 (January 1997)","DOI":"10.1145\/263699.263717"},{"key":"55_CR12","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proc. of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI 2005), pp. 213\u2013223 (June 2005)","DOI":"10.1145\/1065010.1065036"},{"issue":"5","key":"55_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"Software Engineering"},{"key":"55_CR14","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: From code to models. In: Proc. of the Second International Conference on Applications of Concurrency to System Design, ACSD 2001 (June 2001)","DOI":"10.1109\/CSD.2001.981759"},{"key":"55_CR15","unstructured":"Jones, R., Kelly, P.: Backwards-compatible bounds checking for arrays and pointers in C programs. In: Proc. of the International Workshop on Automatic Debugging (1997)"},{"key":"55_CR16","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proc. of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003)","DOI":"10.1007\/3-540-36577-X_40"},{"key":"55_CR17","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Proc. of the 34th annual Design Automation Conference, DAC 1997, pp. 263\u2013268 (1997)","DOI":"10.1145\/266021.266090"},{"key":"55_CR18","unstructured":"Marinov, D., Andoni, A., Daniliuc, D., Khurshid, S., and Rinard, M. An evaluation of exhaustive testing for data structures. Tech. rep., MIT Computer Science and Artificial Intelligence Laboratory Report MIT-LCS-TR-921 (2003)"},{"key":"55_CR19","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: Proc.of the 2006 IEEE\/ACM International Conference on Computer-aided Design, ICCAD 2006, pp. 836\u2013843 (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"55_CR20","doi-asserted-by":"crossref","unstructured":"Person, S., Dwyer, M.B., Elbaum, S., P\u0103s\u0103reanu, C.S.: Differential symbolic execution. In: Proc. of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT \u201908\/FSE-16), pp. 226\u2013237 (2008)","DOI":"10.1145\/1453101.1453131"},{"key":"55_CR21","unstructured":"Ruwase, O., Lam, M.S.: A practical dynamic buffer overflow detector. In: Proc. of the 11th Annual Network and Distributed System Security Symposium, pp. 159\u2013169 (2004)"},{"key":"55_CR22","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: Proc. of the 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE-13), pp. 263\u2013272 (September 2005)","DOI":"10.1145\/1081706.1081750"},{"key":"55_CR23","doi-asserted-by":"crossref","unstructured":"Smith, E.W., Dill, D.L.: Automatic formal verification of block cipher implementations. In: Proc. of the 2008 International Conference on Formal Methods in Computer-Aided Design (FMCAD 2008), pp. 1\u20137 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.10"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_55","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T17:41:08Z","timestamp":1560361268000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}