Abstract
This paper addresses a problem arising in automated proof of invariants of transition systems, for example transition systems modelling distributed programs. Most of the time, the actual properties we want to prove are too weak to hold inductively, and auxiliary invariants need to be introduced. The problem is how to find these extra invariants. We propose a method where we find minimal counter examples to candidate invariants by means of automated random testing techniques. These counter examples can be inspected by a human user, and used to adapt the set of invariants at hand. We are able to find two different kinds of counter examples, either indicating (1) that the used invariants are too strong (a concrete trace of the system violates at least one of the invariants), or (2) that the used invariants are too weak (a concrete transition of the system does not maintain all invariants). We have developed and evaluated our method in the context of formally verifying an industrial-strength implementation of a fault-tolerant distributed leader election protocol.
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
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Armstrong, J.: Programming Erlang – Software for a Concurrent World. The Pragmatic Programmers (2007), http://books.pragprog.com/titles/jaerlang
Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent Programming in Erlang. Prentice-Hall, Englewood Cliffs (1996)
Arts, T., Claessen, K., Svensson, H.: Semi-formal development of a fault-tolerant leader election protocol in Erlang. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 140–154. Springer, Heidelberg (2005)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Berghofer, T., Nipkow, S.: Random testing in isabelle/hol. In: Software Engineering and Formal Methods. SEFM 2004. Proceedings of the Second International Conference, September 28-30, 2004, pp. 230–239 (2004)
Claessen, K.: Equinox, a new theorem prover for full first-order logic with equality. Presentation at Dagstuhl Seminar 05431 on Deduction and Applications (October 2005)
Claessen, K., Hähnle, R., Mårtensson, J.: Verification of hardware systems with first-order logic. In: Proc. of Problems and Problem Sets Workshop (PaPS) (2002)
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of haskell programs. In: ICFP 2000: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pp. 268–279. ACM, New York (2000)
Weidenbach, C., et al.: SPASS: An automated theorem prover for first-order logic with equality, http://spass.mpi-sb.mpg.de
Fredlund, L.-Å., Svensson, H.: McErlang: A model checker for a distributed functional programming language. In: Proc. of International Conference on Functional Programming (ICFP), ACM SIGPLAN, New York (2007)
Garcia-Molina, H.: Elections in a distributed computing system. IEEE Transactions on Computers C-31(1), 48–59 (1982)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)
Hughes, J.: QuickCheck testing for fun and profit. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 1–32. Springer, Heidelberg (2006)
Kaufmann, M., Moore, J.S.: ACL2 - A Computational Logic / Applicative Common Lisp, http://www.cs.utexas.edu/users/moore/acl2/
Schulz, S.: The e equational theorem prover, http://eprover.org
Stark, J., Ireland, A.: Invariant discovery via failed proof attempts. In: Proceedings, 8th International Workshop on Logic Based Program Synthesis and Transformation (1998)
Stoller, S.D.: Leader election in distributed systems with crash failures. Technical Report 481, Computer Science Dept., Indiana University, May 1997. Revised (July 1997)
Svensson, H., Arts, T.: A new leader election implementation. In: ERLANG 2005: Proceedings of the 2005 ACM SIGPLAN workshop on Erlang, pp. 35–39. ACM Press, New York (2005)
Voronkov, A.: Vampire, http://www.vampire.fm
Wordsworth, J.B.: Software Engineering with B. Addison-Wesley, Reading (1996)
Zeller, A.: Isolating cause-effect chains from computer programs. In: SIGSOFT 2002/FSE-10: Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, pp. 1–10. ACM, New York (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Claessen, K., Svensson, H. (2008). Finding Counter Examples in Induction Proofs . In: Beckert, B., Hähnle, R. (eds) Tests and Proofs. TAP 2008. Lecture Notes in Computer Science, vol 4966. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79124-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-79124-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79123-2
Online ISBN: 978-3-540-79124-9
eBook Packages: Computer ScienceComputer Science (R0)