{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T18:34:05Z","timestamp":1761676445228,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319488684"},{"type":"electronic","value":"9783319488691"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","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":[[2016]]},"DOI":"10.1007\/978-3-319-48869-1_5","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T08:41:52Z","timestamp":1478508112000},"page":"56-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Constructing Semantic Models of Programs with the Software Analysis Workbench"],"prefix":"10.1007","author":[{"given":"Robert","family":"Dockins","sequence":"first","affiliation":[]},{"given":"Adam","family":"Foltzer","sequence":"additional","affiliation":[]},{"given":"Joe","family":"Hendrix","sequence":"additional","affiliation":[]},{"given":"Brian","family":"Huffman","sequence":"additional","affiliation":[]},{"given":"Dylan","family":"McNamee","sequence":"additional","affiliation":[]},{"given":"Aaron","family":"Tomb","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-12154-3_4","volume-title":"Verified Software: Theories, Tools and Experiments","author":"W Ahrendt","year":"2014","unstructured":"Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., H\u00e4hnle, R., Hentschel, M., Herda, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P.H., Ulbrich, M.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55\u201371. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-12154-3_4"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2), 7:1\u20137:31 (2015)","DOI":"10.1145\/2701415"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22792-9_5"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.Y.: Implementing TLS with verified cryptographic security. In: Proceedings of the 2013 IEEE Symposium on Security and Privacy (SP), pp. 445\u2013459, May 2013","DOI":"10.1109\/SP.2013.37"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14295-6_5"},{"key":"5_CR6","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Intl. J. Softw. Tools Technol. Transf. 7(3), 212\u2013232 (2005)"},{"key":"5_CR7","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI 2008), pp. 209\u2013224. USENIX Association, Berkeley (2008)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Carter, K., Foltzer, A., Hendrix, J., Huffman, B., Tomb, A.: SAW: the software analysis workbench. In: Proceedings of the 2013 ACM SIGAda Annual Conference on High Integrity Language Technology (HILT 2013), pp. 15\u201318 (2013)","DOI":"10.1145\/2658982.2527277"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Casinghino, C., Sj\u00f6berg, V., Weirich, S.: Combining proofs and programs in a dependently typed language. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POpPL 2014), pp. 33\u201345 (2014)","DOI":"10.1145\/2535838.2535883"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24730-2_15"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03359-9_2"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Erk\u00f6k, L., Matthews, J.: Pragmatic equivalence and safety checking in Cryptol. In: Proceedings of the 3rd Workshop on Programming Languages Meets Program Verification (PLpPV 2009), pp. 73\u201382 (2009)","DOI":"10.1145\/1481848.1481860"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Falke, S., Merz, F., Sinz, C.: The bounded model checker LLBMC. In: Proceedings of the 28th IEEE\/ACM International Conference on Automated Software Engineering, (ASE 2013), pp. 706\u2013709. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693138"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-37036-6_8"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-04694-0_6","volume-title":"Runtime Verification","author":"T Hansen","year":"2009","unstructured":"Hansen, T., Schachte, P., S\u00f8ndergaard, H.: State joining and splitting for the symbolic execution of binaries. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 76\u201392. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04694-0_6"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Hardin, D.S.: Reasoning about LLVM code using Codewalker. In: Proceedings of the 13th International Workshop on the ACL2 Theorem Prover and Its Applications. Electronic Proceedings in Theoretical Computer Science, vol. 192, pp. 79\u201392, October 2015","DOI":"10.4204\/EPTCS.192.7"},{"issue":"7","key":"5_CR17","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)","journal-title":"Commun. ACM"},{"issue":"3","key":"5_CR18","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2012), pp. 193\u2013204 (2012)","DOI":"10.1145\/2345156.2254088"},{"key":"5_CR20","unstructured":"Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research (2008)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Lewis, J., Martin, B.: Cryptol: high assurance, retargetable crypto development and validation. In: Proceedings of the IEEE Military Communications Conference (MILCOM 2003), vol. 2, pp. 820\u2013825, October 2003","DOI":"10.1109\/MILCOM.2003.1290218"},{"key":"5_CR22","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover. In: Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany (2015)"},{"key":"5_CR23","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic - improved. In: Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2012), pp. 78\u201381. IEEE (2012)"},{"key":"5_CR24","unstructured":"Smith, E.W.: Axe: an automated formal equivalence checking tool for programs. Ph.D. thesis, Stanford University (2011)"},{"key":"5_CR25","unstructured":"The Coq development team: The Coq Proof assistant reference manual. LogiCal Project, version 8.0 (2004). http:\/\/coq.inria.fr"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Tristan, J.B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011), pp. 295\u2013305 (2011)","DOI":"10.1145\/1993498.1993533"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48869-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T01:41:54Z","timestamp":1749692514000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48869-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319488684","9783319488691"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48869-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}