Abstract
We argue for the importance of tool integration in achieving the Program Verifier Grand Challenge. In particular, we argue for what we call strong integration, i.e. a co-operative style of interaction between tools. We propose the use of an existing planning technique, called proof planning, as a possible basis for achieving strong integration.
The work discussed was supported in . part by EPSRC grants GR/R24081 and GR/S01771. We are grateful for feedback on this position paper from Alan Bundy. Thanks also goes to Praxis High Integrity Systems Ltd, in particular Peter Amey and Rod Chapman for their support.
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
Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Conference Record of POPL2002: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, pp. 1–3 (2002)
Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)
Baudin, P., Pacalet, A., Raguideau, J., Schoen, D., Williams, N.: Caveat: A tool for software validation. In: International Conference on Dependable Systems and Networks (DSN 2002), IEEE Computer Society Press, Los Alamitos (2002)
Boyer, R.S., Moore, J.S.: Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In: Hayes, J.E., Richards, J., Michie, D. (eds.) Machine Intelligence, vol. 11, pp. 83–124 (1988)
Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, R., Overbeek, R. (eds.) 9th International Conference on Automated Deduction, pp. 111–120. Springer, Heidelberg (1988); Longer version available from Edinburgh as DAI Research Paper No. 349
Bundy, A.: The use of proof plans for normalization. In: Boyer, R.S. (ed.) Essays in Honor of Woody Bledsoe, pp. 149–166. Kluwer, Dordrecht (1991); Also available from Edinburgh as DAI Research Paper No. 513
Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-Clam system. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol. 449, pp. 647–648. Springer, Heidelberg (1990)
de Moura, L., Owre, S., Rueb, H., Rushby, J., Shankar, N.: Integrating verification components: The interface is the message (2005), http://www.csl.sri.com/users/shankar/shankar-drafts.html
Ellis, B.J., Ireland, A.: Automation for exception freedom proofs. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, pp. 343–346. IEEE Computer Society, Los Alamitos (2003); Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0010
Ellis, B.J., Ireland, A.: An integration of program analysis and automated theorem proving. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 67–86. Springer, Heidelberg (2004); Also available from the School of Mathematical and Computer Sciences, Heriot-Watt University, as Technical Report HW-MACS-TR-0014
Flanagan, C., Rustan, K., Leino, M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, Springer, Heidelberg (2001)
Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for Java. In: Proceedings of PLDI (2002)
Gordon, M.J.: HOL: A proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification, Verification and Synthesis, Kluwer, Dordrecht (1988)
Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)
Hall, A., Chapman, R.: Correctness by construction: Developing a commercial secure system. IEEE Software 19(2) (2002)
Ireland, A.: The Use of Planning Critics in Mechanizing Inductive Proofs. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 178–189. Springer, Heidelberg (1992); Also available from Edinburgh as DAI Research Paper 592
Ireland, A., Bundy, A.: Extensions to a Generalization Critic for Inductive Proof. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 47–61. Springer, Heidelberg (1996); Also available from Edinburgh as DAI Research Paper 786
Ireland, A., Bundy, A.: Productive use of failure in inductive proof. Journal of Automated Reasoning 16(1–2), 79–111 (1996); Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh
Ireland, A., Bundy, A.: Automatic Verification of Functions with Accumulating Parameters. Journal of Functional Programming: Special Issue on Theorem Proving & Functional Programming 9(2), 225–245 (1999); A longer version is available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM/97/11
Ireland, A., Ellis, B.J., Cook, A., Chapman, R., Barnes, J.: An integrated approach to high integrity software verification. Journal of Automated Reasoning: Special Issue on Empirically Successful Automated Reasoning 36(4), 379–410 (2006)
Ireland, A., Stark, J.: Proof planning for strategy development. Annals of Mathematics and Artificial Intelligence 29(1-4), 65–97 (2001); An earlier version is available as Research Memo RM/00/3, Dept. of Computing and Electrical Engineering, Heriot-Watt University
King, S., Hammond, J., Chapman, R., Pryor, A.: Is proof more cost effective than testing? IEEE Trans. on SEÂ 26(8) (2000)
MoD. Hazard analysis and safety classification of the computer and programmable electronic system elements of defence equipment. Interim Defence Standard 00-56, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK (April, 1991)
MoD. The procurement of safety critical software in defence equipment (part 1: Requirements, part 2: Guidance). Interim Defence Standard 00-55, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK (April, 1991)
Nguyen, T., Ourghanlian, A.: Dependability assessment of safety-critical system software by static analysis methods. In: International Conference on Dependable Systems and Networks (DSN 2003), IEEE Computer Society Press, Los Alamitos (2003)
PolySpace-Technologies, http://www.polyspace.com/
Slind, K., Boulton, R.: Iterative dialogues and automated proof. In: Proceedings of the Second International Workshop on Frontiers of Combining Systems (FroCoS 1998), Amsterdam, The Netherlands (October, 1998)
Slind, K., Gordon, M., Boulton, R., Bundy, A.: System description: An interface between CLAM and HOL. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, Springer, Heidelberg (1998); Earlier version available from Edinburgh as DAI Research Paper 885
Stark, J., Ireland, A.: Invariant discovery via failed proof attempts. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, Springer, Heidelberg (1999); An earlier version is available from the Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM/98/2
Steel, G.: The importance of non-theorems and counterexamples in program verification. In: Submitted to the IFIP Working Conference on Verified Software: Theories, Tools, Experiments (2005)
Wegbreit, B.: The synthesis of loop predicates. Comm. ACM 17(2), 102–122 (1974)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ireland, A. (2008). Tool Integration for Reasoned Programming. 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_45
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_45
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)