Abstract
In the formal methods approach to software verification, we use logical formulae to model both the program and its intended specification, and, then, we apply (automated) reasoning techniques to demonstrate that the formulae satisfy a verification conjecture. One may either apply proving techniques, to provide a formal verification argument, or disproving techniques to falsify the verification conjecture. However, programs often contain bugs or are flawed, and, so, the verification process breaks down. Interpreting the failed proof attempt or the counterexample, if any, is very valuable, since it potentially helps identifying the program bug or flaw. Lakatos, in his book Proofs and Refutations, argues that the analysis of a failed proof often holds the key for the development of a theory. Proof analysis enables the strengthening of naïve conjectures and concepts, without severely weakening its content. In this paper, we survey our encounters on the productive use of failure in the context of a few theories, natural numbers and (higher-order) lists, and in the context of security protocols.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ahrendt, W.: Deductive search for errors in free data type specifications using model generation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 211–225. Springer, Heidelberg (2002)
Basin, D.A., Mödersheim, S., Viganò, L.: OFMC: A symbolic model checker for security protocols. International Journal of Information Security 4(3), 181–208 (2005)
Bird, R.: Introduction to Functional Programming Using Haskell, 2nd edn. Prentice Hall Europe, Englewood Cliffs (1998)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Computer Security Foundations Workshop, pp. 82–96. IEEE Computer Science Press, Los Alamitos (2001)
Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, R., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988); Also available from Edinburgh as DAI Research Paper No. 349
Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490. Academic Press, London (1980)
Hutter, D., Monroy, R.: On the automated correction of protocols with improper message encoding. In: Degano, P. (ed.) ARSPA-WITS 2009. LNCS, vol. 5511, pp. 138–154. Springer, Heidelberg (2009)
Lakatos, I.: Proofs and refutations: The logic of Mathematical discovery. Cambridge University Press, Cambridge (1976)
López-Pimentel, J.C., Monroy, R., Hutter, D.: A method for patching interleaving-replay attacks in faulty security protocols. Electronic Notes in Theoretical Computer Science 174, 117–130 (2007); Proceedings of the 2006 FLoC Verification and Debugging Workshop
López-Pimentel, J.C., Monroy, R., Hutter, D.: On the automated correction of security protocols susceptible to a replay attack. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 594–609. Springer, Heidelberg (2007)
Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters 56(3), 131–133 (1995)
McCune, W.: Mace4 reference manual and guide. Computer Research Repository cs.SC/0310055 (2003)
Monroy, R., Bundy, A., Ireland, A.: Proof plans for the correction of false conjectures. In: Pfenning, F. (ed.) LPAR 1994. LNCS (LNAI), vol. 822, pp. 54–68. Springer, Heidelberg (1994); Also available from Edinburgh as DAI Research Paper No. 681
Monroy, R.: The use of abduction and recursion-editor techniques for the correction of faulty conjectures. In: Flenner, P., Alexander, P. (eds.) Proceedings of the 15th Conference on Automated Software Engineering, September 11-15, pp. 91–99. IEEE Computer Society Press, Grenoble (2000)
Monroy, R.: Concept formation via proof planning failure. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 718–731. Springer, Heidelberg (2001)
Monroy, R.: Predicate synthesis for correcting faulty conjectures: the proof planning paradigm. Automated Software Engineering 10(3), 247–269 (2003)
Monroy, R., Bundy, A.: On the correction of faulty formulae. Computación y Sistemas 5(1), 25–37 (2001)
Peirce, C.S.: Collected papers of Charles Sanders Peirce. In: Harston, C., Weiss, P. (eds.), vol. 2. Harvard University Press, Cambridge (1959)
Popper, K.: The Logic of Scientific Discovery, vol. 2. Routledge, New York (2002)
Steel, G., Bundy, A.: Attacking group protocols by refuting incorrect inductive conjectures. Automated Reasoning 36(2), 149–176 (2006); Special Issue on Automated Reasoning for Security Protocol Analysis
Steel, G.: The importance of non-theorems and counterexamples in program verification. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 491–495. Springer, Heidelberg (2008)
Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(2-3), 191–230 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Monroy, R. (2010). Some Encounters on the Productive Use of a Failed Proof Attempt or a Counterexample. In: Sidorov, G., Hernández Aguirre, A., Reyes García, C.A. (eds) Advances in Artificial Intelligence. MICAI 2010. Lecture Notes in Computer Science(), vol 6437. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16761-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-16761-4_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16760-7
Online ISBN: 978-3-642-16761-4
eBook Packages: Computer ScienceComputer Science (R0)