{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:07Z","timestamp":1763467987069},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2011,9,1]],"date-time":"2011-09-01T00:00:00Z","timestamp":1314835200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2011,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>A central objective of the verifying compiler grand challenge is to develop a push-button verifier that generates proofs of correctness in a syntax-driven fashion similar to the way an ordinary compiler generates machine code. The software developer\u2019s role is then to provide suitable specifications and annotated code, but otherwise to have no direct involvement in the verification step. However, the general mathematical developments and results upon which software correctness is based may be established through a separate formal proof process in which proofs might be mechanically checked, but not necessarily automatically generated. While many ideas that could conceivably form the basis for software verification have been known \u201cin principle\u201d for decades, and several tools to support an aspect of verification have been devised, practical fully automated verification of full software behavior remains a grand challenge. This paper explains how RESOLVE takes a step towards addressing this challenge by integrating foundational and practical elements of software engineering, programming languages, and mathematical logic into a coherent framework. Current versions of the RESOLVE verifier generate verification conditions (VCs) for the correctness of component-based software in a modular fashion\u2014one component at a time. The VCs are currently verified using automated capabilities of the Isabelle proof assistant, the SMT solver Z3, a minimalist rewrite prover, and some specialized decision procedures. Initial experiments with the tools and further analytic considerations show both the progress that has been made and the challenges that remain.<\/jats:p>","DOI":"10.1007\/s00165-010-0154-3","type":"journal-article","created":{"date-parts":[[2010,4,13]],"date-time":"2010-04-13T16:45:20Z","timestamp":1271177120000},"page":"607-626","source":"Crossref","is-referenced-by-count":42,"title":["Building a push-button RESOLVE verifier: Progress and challenges"],"prefix":"10.1145","volume":"23","author":[{"given":"Murali","family":"Sitaraman","sequence":"first","affiliation":[{"name":"School of Computing, Clemson University, 29634, Clemson, SC, USA"}]},{"given":"Bruce","family":"Adcock","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The Ohio State University, 43210, Columbus, OH, USA"}]},{"given":"Jeremy","family":"Avigad","sequence":"additional","affiliation":[{"name":"Department of Philosophy, Carnegie Mellon University, 15213, Pittsburgh, PA, USA"}]},{"given":"Derek","family":"Bronish","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The Ohio State University, 43210, Columbus, OH, USA"}]},{"given":"Paolo","family":"Bucci","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The Ohio State University, 43210, Columbus, OH, USA"}]},{"given":"David","family":"Frazier","sequence":"additional","affiliation":[{"name":"School of Computing, Clemson University, 29634, Clemson, SC, USA"}]},{"given":"Harvey M.","family":"Friedman","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The Ohio State University, 43210, Columbus, OH, USA"},{"name":"Department of Mathematics, The Ohio State University, 43210, Columbus, OH, USA"}]},{"given":"Heather","family":"Harton","sequence":"additional","affiliation":[{"name":"School of Computing, Clemson University, 29634, Clemson, SC, USA"}]},{"given":"Wayne","family":"Heym","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The Ohio State University, 43210, Columbus, OH, USA"}]},{"given":"Jason","family":"Kirschenbaum","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The Ohio State University, 43210, Columbus, OH, USA"}]},{"given":"Joan","family":"Krone","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, Denison University, 43023, Granville, OH, USA"}]},{"given":"Hampton","family":"Smith","sequence":"additional","affiliation":[{"name":"School of Computing, Clemson University, 29634, Clemson, SC, USA"}]},{"given":"Bruce W.","family":"Weide","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The Ohio State University, 43210, Columbus, OH, USA"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Aichernig BK Larson PG (1997) A proof obligation generator for VDM-SL In: Proc. FME 4 LNCS 1313. Springer New York","DOI":"10.1007\/3-540-63533-5_18"},{"key":"e_1_2_1_2_2_2","unstructured":"Alkassar E Hillebrand M Leinenbach D Schirmer NW Starostin A (2008) The Verisoft approach to system verification. In: Proc. VSTTE 2008. Springer New York"},{"key":"e_1_2_1_2_3_2","volume-title":"High-integrity Ada: the Spark approach","author":"Barnes J","year":"2002"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barnett M Chang BYE et\u00a0al (2006) Boogie: a modular reusable verifier for object-oriented programs. In: de Boer FS Bonsangue MM de Roever W-P (eds) Proc. FMCO 4 LNCS 4111. Springer pp 364\u2013387","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Barnett M Leino KR Schulte W (2004) The Spec# programming system: an overview. In: Burdy L Huisman M (eds) Construction and analysis of safe secure and interoperable smart devices international workshop LNCS 3362. Springer pp 49\u201369","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Barrett C Tinelli C (2007) CVC3. In: Damm W Hermanns H (eds) Proc. CAV 19 LNCS 4590. Springer pp 298\u2013302","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"e_1_2_1_2_7_2","volume-title":"The calculus of computation: decision procedures with applications to verification","author":"Bradley A","year":"2007"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_2_9_2","unstructured":"Cok D (2008) Adapting JML to generic types and Java 1.6. In: Proc. SAVCBS pp 27\u201335. http:\/\/www.eecs.ucf.edu\/SAVCBS\/2008\/SAVCBS08-proceedings.pdf"},{"key":"e_1_2_1_2_10_2","unstructured":"The Coq proof assistant reference manual version v8.1. ftp:\/\/ftp.inria.fr\/INRIA\/coq\/current\/doc\/Reference-Manual.pdf"},{"issue":"5","key":"e_1_2_1_2_11_2","first-page":"50","article-title":"Reasoning about method calls in interface specifications","volume":"5","author":"Darvas \u00c1","year":"2006","journal-title":"J Object Technol (JOT)"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"de Moura L Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: Proc. TACAS pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_13_2","unstructured":"Detlefs DL Leino KRM Nelson G Saxe JB (1998) Extended static checking. Research Report 159 Compaq Systems Research Center"},{"issue":"2","key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","article-title":"Simplify: a theorem prover for program checking","volume":"52","author":"Detlefs D","year":"2005","journal-title":"JACM"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.277576"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpa.3160330503"},{"key":"e_1_2_1_2_17_2","unstructured":"Filli\u00e2tre J March\u00e9 C (2007) The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm W Hermanns H (eds) Proc. CAV 19 LNCS 4590. Springer New York"},{"key":"e_1_2_1_2_18_2","unstructured":"Friedman HM (2009) Deciding statements about strings with applications to program verification. OSU-CISRC-8\/09-TR42 Department of Computer Science and Engineering The Ohio State University"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-007-9078-x"},{"key":"e_1_2_1_2_20_2","first-page":"1395","article-title":"Formal proof\u2014theory and practice","volume":"55","author":"Harrison J","year":"2008","journal-title":"Notices of the AMS"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.90445"},{"key":"e_1_2_1_2_22_2","volume-title":"Wiley Encyclopedia of Computer Science and Engineering.","author":"Harton HK","year":"2008"},{"key":"e_1_2_1_2_23_2","unstructured":"Heym W (1995) Computer program verification: improvements for human reasoning. Ph.D. thesis The Ohio State University"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_2_1_2_26_2","unstructured":"Hoare CAR Misra J Leavens GT Shankar N (2007) The verified software initiative: a manifesto http:\/\/qpq.csl.sri.com\/vsr\/manifesto.pdf\/vie.. Accessed December 2008"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hollingsworth JE Blankenship L Weide BW (2000) Experience report: using RESOLVE\/C++ for commercial software. In: Schneir B (ed) Proc. FSE. ACM pp 11\u201319","DOI":"10.1145\/357474.355048"},{"key":"e_1_2_1_2_28_2","unstructured":"Jackson D (2006) Software abstractions: logic language and analysis. MIT Press Cambridge"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.2003.1203057"},{"key":"e_1_2_1_2_30_2","unstructured":"Karabotsos G Chalin P James PR Giannas L (2008) Total correctness of recursive functions using JML4 FSPV. In: Proc. SAVCBS pp 19\u201327. http:\/\/www.eecs.ucf.edu\/SAVCBS\/2008\/SAVCBS08-proceedings.pdf"},{"key":"e_1_2_1_2_31_2","unstructured":"King JC (1970) A Program Verifier. Ph.D. dissertation Carnegie Tech 261\u00a0pp"},{"key":"e_1_2_1_2_32_2","unstructured":"Kirschenbaum J Harton HK Sitaraman M (2008) A case study in automated verification. In: Shankar N (ed) Proc. CAV AFM Workshop"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Kirschenbaum J Adcock B Bronish D Smith H Harton H Sitaraman M Weide BW (2009) Verifying component-based software: deep mathematics or simple bookkeeping? In: Edwards SH Kulczycki G (eds) Proc. ICSR 11 LNCS 5791. Springer pp 31\u201340","DOI":"10.1007\/978-3-642-04211-9_4"},{"key":"e_1_2_1_2_34_2","unstructured":"Krone J (1988) The role of verification in software reusability. Ph.D. Thesis The Ohio State University"},{"key":"e_1_2_1_2_35_2","volume-title":"Wiley Encyclopedia of Computer Science and Engineering.","author":"Kulczycki G","year":"2008"},{"key":"e_1_2_1_2_36_2","unstructured":"Kulczycki G (2004) Direct reasoning Ph.D. Dissertation Clemson University"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1145\/1118537.1123066","article-title":"A specification-based approach to reasoning about pointers","volume":"31","author":"Kulczycki G","year":"2006","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Leavens GT Abrial J-R Batory D Butler M Coglio A Fisler K Hehner E Jones C Miller D Peyton-Jones S Sitaraman M Smith DR Stump A (2006) Roadmap for enhanced languages and methods to aid verification. In: Proc. GPCE 5. ACM Press New York pp 221\u2013236","DOI":"10.1145\/1173706.1173740"},{"issue":"2","key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","article-title":"Specification and verification challenges for sequential object-oriented programs","volume":"19","author":"Leavens GT","year":"2008","journal-title":"Formal Aspects Comput"},{"key":"e_1_2_1_2_41_2","first-page":"2","article-title":"Towards the formal verification of a C0 compiler: code generation and implementation correctness","volume":"3","author":"Leinenbach D","year":"2005","journal-title":"SEFM"},{"key":"#cr-split#-e_1_2_1_2_42_2.1","unstructured":"Leino KRM M\u00fcller P Wallenburg A (2008) Flexible immutability with frozen objects. In: Shankar N"},{"key":"#cr-split#-e_1_2_1_2_42_2.2","unstructured":"(ed) Proc. VSTTE 2008 LNCS 5295. Springer New York pp 192-208"},{"key":"e_1_2_1_2_43_2","unstructured":"Leino KRM M\u00fcller P (2008) Using the Spec# language methodology and tools to write bug-free programs. LASER 2007\/2008 Lecture Notes Springer New York"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Leino KRM (2010) Dafny: An automated program verifier for functional correctness. In: Proc. LPAR 16 (in press)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_2_46_2","volume-title":"Foundations of component-based systems.","author":"M\u00fcller P","year":"2000"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Nipkow T Paulson LC Wenzel M (2002) Isabelle\/HOL: a proof assistant for higher-order logic. LNCS 2283. Springer New York","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Owre S Rajan SP Rushby JM Shankar N Srivas M (1996) PVS: combining specification proof checking and model checking. In: Alur R Henzinger TA (eds) Proc. CAV LNCS 1102. Springer Berlin pp 411\u2013414","DOI":"10.1007\/3-540-61474-5_91"},{"key":"e_1_2_1_2_49_2","first-page":"91","article-title":"The design and implementation of VAMPIRE.","volume":"15","author":"Riazanov A","year":"2002","journal-title":"AI Commun"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Schulz S (2004) System abstract: E 0.81. In: Proc. 2nd IJCAR. LNAI 3097. Springer Berlin pp 223\u2013228","DOI":"10.1007\/978-3-540-25984-8_15"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/190679.199221"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.585503"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Sitaraman M Atkinson S Kulczycki G Weide B Long T Bucci P Pike S Heym W Hollingsworth J (2000) Reasoning about software-component behavior. In: Proc. ICSR 6 LCNS 1844. Springer Berlin pp 266\u2013283","DOI":"10.1007\/978-3-540-44995-9_16"},{"key":"e_1_2_1_2_54_2","unstructured":"Smith H Roche K Sitaraman M Krone J Ogden WF (2008) Integrating math units and proof checking for specification and verification. In: Proc. SAVCBS pp 59\u201366. http:\/\/www.eecs.ucf.edu\/SAVCBS\/2008\/SAVCBS08-proceedings.pdf"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Smith H Harton H Frazier D Mohan R Sitaraman M (2009) Generating verified Java components through RESOLVE. In: Edwards SH Kulczycki G (eds) Proc. ICSR 11 LNCS 5791. Springer Berlin pp 11\u201320","DOI":"10.1007\/978-3-642-04211-9_2"},{"key":"#cr-split#-e_1_2_1_2_56_2.1","unstructured":"Weide BW Sitaraman M Harton HK Adcock B Bucci P Bronish D Heym WD Kirschenbaum J Frazier D (2008) Incremental benchmarks for software verification tools and techniques. In: Shankar N"},{"key":"#cr-split#-e_1_2_1_2_56_2.2","unstructured":"(ed) Proc. VSTTE 2008 LNCS 5295. Springer Berlin pp 84-98"},{"key":"e_1_2_1_2_57_2","unstructured":"Weide BW Heym W (2001) Specification and verification with references. In: Proc. SAVCBS pp 50\u201359"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.310672"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Zee K Kuncak V Rinard M C (2008) Full functional verification of linked data structures. In: Proc. PLDI. ACM Press New York pp 349\u2013361","DOI":"10.1145\/1379022.1375624"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Zee K Kuncak V Rinard MC (2009) An integrated proof language for imperative programs. In: Proc. PLDI. ACM Press New York pp 338\u2013351","DOI":"10.1145\/1543135.1542514"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-010-0154-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-010-0154-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-010-0154-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:51:40Z","timestamp":1641484300000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-010-0154-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9]]},"references-count":63,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2011,9]]}},"alternative-id":["10.1007\/s00165-010-0154-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-010-0154-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,9]]}}}