Article

Free access

A framework for combining analysis and verification

Authors:

Răzvan VoicuAuthors Info & Claims

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

Pages 26 - 39

https://doi.org/10.1145/325694.325700

Published: 05 January 2000 Publication History

Abstract

We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis.

In this paper, we start with a representation of a program, user assertions, and a given analyzer for the program. The framework we describe induces an algorithm which exploits the assertions and the analyzer to produce a generally more accurate analysis. Further, it has some important features:

it is flexible: any number of assertions can be used anywhere;

it is open: it can employ an arbitrary analyzer;

it is modular: we reason with conditional correctness of assertions;

it is incremental: it can be tuned for the accuracy/efficiency tradeoff.

References

[1]

Alexander Aiken and Manuel F~hndrich, "Program Analysis Using Mixed Term and Set Constraints", Fourth International Static Analyses Symposium, Paris, France, September 1997.]]

Digital Library

[2]

A. W. Appel, "Modern compiler implementation in ML", Chapter 17.3, Cambridge University Press, 1998.]]

Digital Library

[3]

P. Cousot and R. Cousot, "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints", Proc. 4th A CM Syrup. on Principles of Programming Languages, Los Angeles, 238-252, January 1977.]]

Digital Library

[4]

P. Cousot and R. Cousot, "Systematic Design of Program Analysis Frameworks", Proc. 6th A CM Syrup. on Principles of Programming Languages, San Antonio, 269-282, January 1979.]]

Digital Library

[5]

P. Cousot. Methods and Logics for Proving Programs. In J. van Leeuwen, editor, Formal Models and Semantics~ volume B of Handbook of Theoretical Computer Science, chapter 15, Elsevier, 843-993, 1990.]]

Digital Library

[6]

P. Cousot and R. Cousot. "Abstract Interpretation Frameworks" Journal of Logic and Computation, 2(4), 511-547, August 1992.]]

[7]

D. Gries, "Science of Programming", Springer-Verlag, 1991.]]

[8]

K. Havelund and N. Shankar, "Experiments in Theorem Proving and Model Checking for Protocol Verification", Proceedings of Formal Methods in Europe, 1996.]]

Digital Library

[9]

N. Heintze, "Set Based Program Analysis", Ph.D. thesis, School of Computer Science, Carnegie Mellon University, October 1992.]]

Digital Library

[10]

N. Heintze and J. Jaffar, "A Generic Algorithm for CLP Analysis", 12th International Conference on Logic Programming, 49-63, 1995.]]

[11]

N. Heintze and J. Jaffar, "An Engine for Logic Program Analysis", Proc. 7th IEEE Syrup. on Logic in Computer Science, pp 318-328, 1992.]]

[12]

J. Jaffar and J.-L. Lassez, "Constraint Logic Programming", Proc. 14th A CM Syrup. on Principles of Programming Languages, 1987, pp 111-119.]]

Digital Library

[13]

N. Jones and S. Muchnick, "A Flexible Approach to Interprocedural Dataflow Analysis and Programs with Recursive Data Structures", Proc. 9th A CM Symp. on Principles of Programming Languages, pp. 244-256, January 1982.]]

Digital Library

[14]

Greg Nelson and Derek C. Oppen, "Simplification by cooperating decision procedures", ACM Transactions on Programming Languages and Systems, t(2), pp 245-257, October 1979.]]

Digital Library

[15]

Sam Owre, John M. Rushby, and Natarajan Shankar, PVS: A Prototype Verification System", in Deepak Kapur, editor, Automated Deduction- CADE-II, l lth International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Springer- Verlag, 748- 752, June 1992.]]

Digital Library

[16]

V. Rusu and E. Singerman, "On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction", 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1579, Springer-Verlag, March 1999.]]

Digital Library

[17]

S. Graf and H. Saidi, "Verifying Invariants Using Theorem Proving" Proc. 8th Int. Conf. on Computer Aided Verification, 196-207, 1996.]]

Digital Library

[18]

S. Bensalem, Y. Lakhnech, S. Saidi, "Powerful Techniques for the Automatic Generation of Invariants" Proc. 8~h Int. Conf. on Computer Aided Verification, 323-335, 1996.]]

Digital Library

Cited By

Kirchner FKosmatov NPrevosto VSignoles JYakobowski B(2015)Frama-C: A software analysis perspectiveFormal Aspects of Computing10.1007/s00165-014-0326-727:3(573-609)Online publication date: 9-Jan-2015
https://doi.org/10.1007/s00165-014-0326-7
Correnson LSignoles J(2012)Combining Analyses for C Program VerificationFormal Methods for Industrial Critical Systems10.1007/978-3-642-32469-7_8(108-130)Online publication date: 2012
https://doi.org/10.1007/978-3-642-32469-7_8
Bai YBrandt JSchneider KCorporaal HStuijk S(2011)SMT-based optimization for synchronous programsProceedings of the 14th International Workshop on Software and Compilers for Embedded Systems10.1145/1988932.1988935(11-20)Online publication date: 27-Jun-2011
https://dl.acm.org/doi/10.1145/1988932.1988935
Show More Cited By

Index Terms

A framework for combining analysis and verification
1. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning
    2. Program semantics

Recommendations

Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The ...
Verifying the Verifier: eBPF Range Analysis Verification
Computer Aided Verification
Abstract
This paper proposes an automated method to check the correctness of range analysis used in the Linux kernel ’s eBPF verifier. We provide the specification of soundness for range analysis performed by the eBPF verifier. We automatically generate ...
Temporal property verification as a program analysis task

We describe a reduction from temporal property verification to a program analysis problem. First we present a proof system that, unlike the standard formulation, is more amenable to reasoning about infinite-state systems: disjunction is treated by ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

January 2000

402 pages

ISBN:1581131259

DOI:10.1145/325694

Chairmen:
Mark Wegman
IBM T. J. Watson Research Center, Yorktown Heights, NY
,
Thomas Reps
Univ. of Wisconsin

Copyright © 2000 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 January 2000

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL00

Sponsor:

POPL00: Symposium on Principles of Programming Languages 2000

January 19 - 21, 2000

MA, Boston, USA

Acceptance Rates

POPL '00 Paper Acceptance Rate 30 of 151 submissions, 20%;

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

6
Total Citations
View Citations
492
Total Downloads

Downloads (Last 12 months)63
Downloads (Last 6 weeks)15

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kirchner FKosmatov NPrevosto VSignoles JYakobowski B(2015)Frama-C: A software analysis perspectiveFormal Aspects of Computing10.1007/s00165-014-0326-727:3(573-609)Online publication date: 9-Jan-2015
https://doi.org/10.1007/s00165-014-0326-7
Correnson LSignoles J(2012)Combining Analyses for C Program VerificationFormal Methods for Industrial Critical Systems10.1007/978-3-642-32469-7_8(108-130)Online publication date: 2012
https://doi.org/10.1007/978-3-642-32469-7_8
Bai YBrandt JSchneider KCorporaal HStuijk S(2011)SMT-based optimization for synchronous programsProceedings of the 14th International Workshop on Software and Compilers for Embedded Systems10.1145/1988932.1988935(11-20)Online publication date: 27-Jun-2011
https://dl.acm.org/doi/10.1145/1988932.1988935
Seo SYang HYi K(2003)Automatic Construction of Hoare Proofs from Abstract Interpretation ResultsProgramming Languages and Systems10.1007/978-3-540-40018-9_16(230-245)Online publication date: 2003
https://doi.org/10.1007/978-3-540-40018-9_16
Anderson H(2002)Abstract Interpretation with a Theorem ProverFormal Methods and Software Engineering10.1007/3-540-36103-0_43(411-422)Online publication date: 10-Oct-2002
https://doi.org/10.1007/3-540-36103-0_43
Celiku Ovon Wright J(2002)Theorem Prover Support for Precondition and Correctness CalculationFormal Methods and Software Engineering10.1007/3-540-36103-0_32(299-310)Online publication date: 10-Oct-2002
https://doi.org/10.1007/3-540-36103-0_32

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents