{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:43Z","timestamp":1776305383043,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030025076","type":"print"},{"value":"9783030025083","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-02508-3_17","type":"book-chapter","created":{"date-parts":[[2018,10,13]],"date-time":"2018-10-13T14:22:47Z","timestamp":1539440567000},"page":"313-332","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Symbolic Computation via Program Transformation"],"prefix":"10.1007","author":[{"given":"Henrich","family":"Lauko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,15]]},"reference":[{"key":"17_CR1","series-title":"Addison-Wesley Series in Computer Science","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"2007","unstructured":"Aho, A.V.: Compilers: Principles, Techniques, and Tools. Addison-Wesley Series in Computer Science. Pearson\/Addison Wesley, Boston (2007)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-28756-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 157\u2013172. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-28756-5_12"},{"key":"17_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: SMT-LIB: the satisfiability modulo theories library. \n                      http:\/\/www.smt-lib.org\/"},{"issue":"2","key":"17_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2888393","volume":"25","author":"Petr Bauch","year":"2016","unstructured":"Bauch, P., Havel, V., Barnat, J.: Control explicit-data symbolic model checking. ACM Trans. Softw. Eng. Methodol. 25(2) (2016). Article no. 15. \n                      https:\/\/doi.org\/10.1145\/2888393","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1007\/978-3-662-49674-9_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2016","unstructured":"Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887\u2013904. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49674-9_55"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"17_CR7","unstructured":"Beyer, D., L\u00f6we, S.: Interpolation for value analysis. In: A\u00dfmann, U., Demuth, B., Spitta, T., P\u00fcschel, G., Kaiser, R. (eds.) Software Engineering and Management. Lecture Notes in Informatics, vol. 239, pp. 73\u201374. Gesellschaft f\u00fcr Informatik, Bonn (2015). \n                      https:\/\/dl.gi.de\/handle\/20.500.12116\/2495"},{"issue":"5","key":"17_CR8","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"B Beyer","year":"2007","unstructured":"Beyer, B., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5), 505\u2013525 (2007). \n                      https:\/\/doi.org\/10.1007\/s10009-007-0044-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. In: Proceedings of 23rd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2008, L\u2019Aquila, September 2008, pp. 443\u2013446. IEEE CS Press, Washington, DC (2008). \n                      https:\/\/doi.org\/10.1109\/ase.2008.69","DOI":"10.1109\/ase.2008.69"},{"key":"17_CR10","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of 8th USENIX Symposium on Operating Systems Design and Implementation, San Diego, CA, December 2008, pp. 209\u2013224. USENIX Association (2008). \n                      http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-662-54580-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Chalupa","year":"2017","unstructured":"Chalupa, M., Vitovsk\u00e1, M., Jon\u00e1\u0161, M., Slaby, J., Strej\u010dek, J.: Symbiotic 4: beyond reachability. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 385\u2013389. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54580-5_28"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-26287-1_6","volume-title":"Hardware and Software: Verification and Testing","author":"J Daniel","year":"2015","unstructured":"Daniel, J., Par\u00edzek, P.: PANDA: simultaneous predicate abstraction and concrete execution. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 87\u2013103. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-26287-1_6"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52"},{"issue":"4","key":"17_CR16","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Int. J. Softw. Tools Technol. Transfer 2(4), 366\u2013381 (2000). \n                      https:\/\/doi.org\/10.1007\/s100090050043","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Khurshid","year":"2003","unstructured":"Khurshid, S., P\u0103s\u0103reanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553\u2013568. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-36577-X_40"},{"issue":"7","key":"17_CR18","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). \n                      https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation. In: Proceedings of 2nd IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2004, Palo Alto, CA, March 2004, pp. 75\u201388. IEEE CS Press, Washington, DC (2004). \n                      https:\/\/doi.org\/10.1109\/cgo.2004.1281665","DOI":"10.1109\/cgo.2004.1281665"},{"key":"17_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993). \n                      https:\/\/doi.org\/10.1007\/978-1-4615-3190-6"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-319-32582-8_14","volume-title":"Model Checking Software","author":"J Mr\u00e1zek","year":"2016","unstructured":"Mr\u00e1zek, J., Bauch, P., Lauko, H., Barnat, J.: SymDIVINE: tool for control-explicit data-symbolic state space exploration. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 208\u2013213. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-32582-8_14"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213\u2013228. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45937-5_16"},{"key":"17_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). \n                      https:\/\/doi.org\/10.1007\/978-3-662-03811-6"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/11817963_38","volume-title":"Computer Aided Verification","author":"K Sen","year":"2006","unstructured":"Sen, K., Agha, G.: CUTE and jCUTE: concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 419\u2013423. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11817963_38"},{"key":"17_CR26","doi-asserted-by":"publisher","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of Joint 10th European Software Engineering Conference and 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC\/FSE 2005, Lisbon, September 2005, pp. 263\u2013272. ACM Press, New York (2005). \n                      https:\/\/doi.org\/10.1145\/1081706.1081750","DOI":"10.1145\/1081706.1081750"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-63390-9_11","volume-title":"Computer Aided Verification","author":"M Sousa","year":"2017","unstructured":"Sousa, M., Rodr\u00edguez, C., D\u2019Silva, V., Kroening, D.: Abstract interpretation with unfoldings. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 197\u2013216. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63390-9_11"},{"key":"17_CR28","unstructured":"Wei\u00dfenbacher, G.: Program analysis with interpolants. Ph.D. thesis, University of Oxford (2010)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2018"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02508-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T02:49:17Z","timestamp":1583203757000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02508-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030025076","9783030025083"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02508-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"15 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stellenbosch","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"South Africa","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.ictac.org.za\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}