Abstract
This paper reviews some common knowledge about establishing correctness of programs and the current status of program specification and verification. While doing so, it identifies several challenges related to the grand challenge of building a verifying compiler. The paper argues that invariants are central to establishing correctness of programs and that thus, a major part of an automatic program verifier must be automated support for verifying invariants, a significant problem in itself. The paper discusses where the invariants come from, what can be involved in establishing that they hold, and the extent to which the process of finding and proving invariants can be automated. The paper also discusses several of the related challenges identified, argues that addressing them would make the significance to global program behavior of feedback from a verifying compiler clearer, and recommends that many of them should be included within the scope of the grand challenge.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and Artificial Intelligence 29(1-4), 139–181 (2001)
Archer, M.: Proving correctness of the basic TESLA multicast stream authentication protocol with TAME. In: Workshop on Issues in the Theory of Security (WITS 2002), Portland, OR, January 14–15 (2002)
Archer, M., Heitmeyer, C., Riccobene, E.: Proving invariants of I/O automata with TAME. Automated Software Engineering 9(3), 201–232 (2002)
Bjørner, N., Browne, I.A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoretical Computer Science 173(1), 49–87 (1997)
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence 62, 185–253 (1993)
Bundy, A.: The use of proof plans for normalization. In: Boyer, R.S. (ed.) Automated Reasoning: Essays in Honor of Woody Bledsoe. Automated Reasoning Series, vol. 7, pp. 149–166. Kluwer, Dordrecht (1991)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–583 (1969)
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–169. Springer, Heidelberg (2000)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 1977 Symp. on Principles of Programming Languages (January, 1977)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables. In: Proc. 1978 Symp. on Principles of Programming Languages (January, 1978)
Ernst, M.: Dynamically Discovering Likely Program Invariants. PhD thesis, Univ. of Washington (2000)
Floyd, R.W.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics. Mathematical Aspects of Computer Science, vol. 19, pp. 19–32. American Mathematical Society, Providence, RI (1967)
Garland, S.: TIOA User Guide and Reference Manual. Technical report, MIT CSAIL, Cambridge, MA, URL (2006), http://tioa.csail.mit.edu
Heitmeyer, C., Archer, M., Bharadwaj, R., Jeffords, R.: Tools for constructing requirements specifications: The SCR toolset at the age of ten. International Journal on Computer System Science and Engineering 20(1), 19–35 (2005)
Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. In: Proc. 6th International Symposium on the Foundations of Software Engineering (FSE-6), Orlando, FL (November 1998)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: Case Studies. Kluwer Academic Publishers, Dordrecht (2000)
Kaynar, D., Lynch, N.A., Segala, R., Vaandrager, F.: A mathematical framework for modeling and analyzing real-time systems. In: The 24th IEEE Intern. Real-Time Systems Symposium (RTSS), Cancun, Mexico (December 2003)
Kerber, M., Kohlhase, M., Sorge, V.: Integrating computer algebra into proof planning. Journal of Automated Reasoning 21(3), 327–355 (1998)
Kirby Jr., J., Archer, M., Heitmeyer, C.: SCR: A practical approach to building a high assurance COMSEC system. In: Proc. 15th Annual Computer Security Applications Conference (ACSAC 1999), IEEE Comp. Soc. Press, Los Alamitos (1999)
Lynch, N., Tuttle, M.: An introduction to Input/Output automata. CWI-Quarterly 2(3), 219–246 (1989)
Lynch, N., Vaandrager, F.: Forward and backward simulations – Part II: Timing-based systems. Information and Computation 128(1), 1–25 (1996)
Mitra, S., Archer, M.: PVS strategies for proving abstraction properties of automata. Electronic Notes in Theor. Comp. Sci. 125(2), 45–65 (2005)
Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Prover Guide, Version 2.4. Technical report, Comp. Sci. Lab. SRI Intl. Menlo Park, CA (November 2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Archer, M. (2008). Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)