Article

Avoiding exponential explosion: generating compact verification conditions

Authors:

Cormac Flanagan,

James B. SaxeAuthors Info & Claims

POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 193 - 205

https://doi.org/10.1145/360204.360220

Published: 01 January 2001 Publication History

Get Access

Abstract

Current verification condition (VC) generation algorithms, such as weakest preconditions, yield a VC whose size may be exponential in the size of the code fragment being checked. This paper describes a two-stage VC generation algorithm that generates compact VCs whose size is worst-case quadratic in the size of the source fragment, and is close to linear in practice.This two-stage VC generation algorithm has been implemented as part of the Extended Static Checker for Java. It has allowed us to check large and complex methods that would otherwise be impossible to check due to time and space constraints.

References

[1]

Bowen Alpern, Mark N. Wegman, and F. Kenneth Zadeck. Detecting Equality of Variables in Programs. In 15th ACM Symposium on Principles of Programming Languages, pages 1-11, January 1988.

Digital Library

Google Scholar

[2]

Thomas Ball and Sriram K. Rajamani. Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research, 2000.

Google Scholar

[3]

Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.

Digital Library

Google Scholar

[4]

Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. An Efficient Method of Computing Static Single Assignment Form. In 16th Annual ACM Symposium on Principles of Programming Languages, pages 25-35, January 1989.

Digital Library

Google Scholar

[5]

Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, N J, 1976.

Digital Library

Google Scholar

[6]

David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, December 1998. Available from research, compaq. com/SRC/publications.

Google Scholar

[7]

David L. Detlefs, Greg Nelson, and James B. Saxe. An automatic theoremprover for program checking, to appear 2001.

Google Scholar

[8]

Extended Static Checking web page, Compaq Systems Research Center. On the Web at research, compaq, com/SRC/esc/.

Google Scholar

[9]

K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC/Java user's manual. Compaq Systems Research Center Technical Note 2000-002, October 2000. Available from research, compaq, cora/SRC/ publications.

Google Scholar

[10]

K. Rustan M. Leino, James B. Saxe, and Raymie Stata. Checking Java programs via guarded commands. In Bart Jacobs, Gary T. Leavens, Peter Mfiller, and Arnd Poetzsch-Heffter, editors, Formal Techniques for Java Programs, Technical Report 251. Fernuniversitat Hagen, May 1999. Also available as Compaq Systems Research Center Technical Note 1999-002, from research, compaq. com/SRC/publicat ions.

Digital Library

Google Scholar

[11]

George C. Necula. Translation validation for an optimizing compiler. In Proceedings of the ACM SIGPLAN'98 Conference on Programming Language Design and Implementation, pages 83- 94, June 2000.

Digital Library

Google Scholar

[12]

Greg Nelson. Techniques for program verification. Technical Report CSL-81- 10, Xerox Pale Alto Research Center, 1981.

Google Scholar

[13]

Greg Nelson. A generalization of Dijkstra's calculus. A CM Transactions on Programming Languages and Systems, 11(4):517-561, 1989.

Digital Library

Google Scholar

[14]

George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In Proceedings of the ACM SIGPLAN'00 Conference on Programming Language Design and Implementation, pages 333-344, June 1998.

Digital Library

Google Scholar

Cited By

View all

Saan SSchwarz MErhard JSeidl HTilscher SVojdani V(2024)Correctness Witness Validation by Abstract InterpretationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_4(74-97)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50524-9_4
Ly DKosmatov NLoulergue FSignoles J(2023)Sound Runtime Assertion Checking for Memory Properties via Program TransformationFormal Aspects of Computing10.1145/360595136:1(1-46)Online publication date: 31-Jul-2023
https://dl.acm.org/doi/10.1145/3605951
Lu KLow DTomb A(2023)Constructing Structured SSA from FJProceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3605156.3606457(58-64)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1145/3605156.3606457
Show More Cited By

Index Terms

Avoiding exponential explosion: generating compact verification conditions

Recommendations

Avoiding exponential explosion: generating compact verification conditions

Current verification condition (VC) generation algorithms, such as weakest preconditions, yield a VC whose size may be exponential in the size of the code fragment being checked. This paper describes a two-stage VC generation algorithm that generates ...
Ameliorating the State Explosion Problem
Ameliorating the state explosion problem

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2001

304 pages

ISBN:1581133367

DOI:10.1145/360204

Chairmen:
Chris Hankin
Imperial College, London, U. K.
,
Dave Schmidt
Kansas State Univ., Manhattan

ACM SIGPLAN Notices Volume 36, Issue 3
March 2001
303 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/373243
Editors:
Cindy Norris
Appalachian State Univ., Boone, NC
,
James B. Fenwick
Appalachian State Univ., Boone, NC
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2001

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL01

Sponsor:

POPL01: The 28th Annual ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages

London, United Kingdom

Acceptance Rates

POPL '01 Paper Acceptance Rate 24 of 126 submissions, 19%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

178
Total Citations
View Citations
1,144
Total Downloads

Downloads (Last 12 months)49
Downloads (Last 6 weeks)6

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Saan SSchwarz MErhard JSeidl HTilscher SVojdani V(2024)Correctness Witness Validation by Abstract InterpretationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50524-9_4(74-97)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50524-9_4
Ly DKosmatov NLoulergue FSignoles J(2023)Sound Runtime Assertion Checking for Memory Properties via Program TransformationFormal Aspects of Computing10.1145/360595136:1(1-46)Online publication date: 31-Jul-2023
https://dl.acm.org/doi/10.1145/3605951
Lu KLow DTomb A(2023)Constructing Structured SSA from FJProceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3605156.3606457(58-64)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1145/3605156.3606457
Zhang JLiu SWang XLi TLiu YBissyandé TKlein JBird CSarro F(2023)Learning to Locate and Describe VulnerabilitiesProceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE56229.2023.00045(332-344)Online publication date: 11-Nov-2023
https://dl.acm.org/doi/10.1109/ASE56229.2023.00045
Kalita PSingal DAgarwal PJhunjhunwala SRoy S(2023)Symbolic encoding of LL(1) parsing and its applicationsFormal Methods in System Design10.1007/s10703-023-00420-361:2-3(338-379)Online publication date: 22-Jun-2023
https://doi.org/10.1007/s10703-023-00420-3
Amilon JEsen ZGurov DLidström CRümmer P(2023)Automatic Program Instrumentation for Automatic VerificationComputer Aided Verification10.1007/978-3-031-37709-9_14(281-304)Online publication date: 17-Jul-2023
https://doi.org/10.1007/978-3-031-37709-9_14
Keuchel SHuyghebaert SLukyanov GDevriese D(2022)Verified symbolic execution with Kripke specification monads (and no meta-programming)Proceedings of the ACM on Programming Languages10.1145/35476286:ICFP(194-224)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547628
Blatter LKosmatov NPrevosto VLe Gall P(2022)An Efficient VCGen-Based Modular Verification of Relational PropertiesLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_28(498-516)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19849-6_28
Blatter LKosmatov NPrevosto VLe Gall P(2022)Certified Verification of Relational PropertiesIntegrated Formal Methods10.1007/978-3-031-07727-2_6(86-105)Online publication date: 1-Jun-2022
https://doi.org/10.1007/978-3-031-07727-2_6
Godboley SJaffar JMaghareh RDutta ACadar CZhang X(2021)Toward optimal mc/dc test case generationProceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3460319.3464841(505-516)Online publication date: 11-Jul-2021
https://dl.acm.org/doi/10.1145/3460319.3464841
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Avoiding exponential explosion: generating compact verification conditions

Ameliorating the State Explosion Problem

Ameliorating the state explosion problem