Abstract
HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.
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
HipSpec evaluation results, http://www.cse.chalmers.se/~danr/hipspec
HipSpec source code repository, http://www.github.com/danr/hipspec
Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: meta-level guidance for mathematical reasoning. Cambridge University Press (2005)
Chamarthi, H.R., Dillinger, P., Manolios, P., Vroon, D.: The ACL2 Sedan theorem proving system. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 291–295. Springer, Heidelberg (2011)
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of ICFP, pp. 268–279 (2000)
Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: Guessing formal specifications using testing. In: Proceedings of TAP, pp. 6–21 (2010)
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Dixon, L., Fleuriot, J.D.: Higher order rippling in isaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 83–98. Springer, Heidelberg (2004)
Ireland, A., Bundy, A.: Productive use of failure in inductive proof. Journal of Automated Reasoning 16, 79–111 (1996)
Johansson, M., Dixon, L., Bundy, A.: Case-analysis for rippling and inductive proof. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 291–306. Springer, Heidelberg (2010)
Johansson, M., Dixon, L., Bundy, A.: Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery. In: Siegler, S., Wasser, N. (eds.) Walther Festschrift. LNCS, vol. 6463, pp. 102–116. Springer, Heidelberg (2010)
Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. Journal of Automated Reasoning 47(3), 251–289 (2011)
Kaufmann, M., Panagiotis, M., Moore, S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (2000)
Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315–331. Springer, Heidelberg (2012)
McCasland, R., Bundy, A., Autexier, S.: Automated discovery of inductive theorems. In: Matuszewski, R., Rudnicki, P. (eds.) From Insight to Proof: Festschrift in Honor of A. Trybulec (2007)
Montano-Rivas, O., McCasland, R., Dixon, L., Bundy, A.: Scheme-based theorem discovery and concept invention. Expert Systems with Applications 39(2), 1637–1646 (2012)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Rosén, D.: Proving Equational Haskell Properties using Automated Theorem Provers, MSc. Thesis, University of Gothenburg (2012)
Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: An automated prover for properties of recursive data structures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407–421. Springer, Heidelberg (2012)
Vytiniotis, D., Rosén, D., Peyton Jones, S., Claessen, K.: HALO: Haskell to logic through denotational semantics. In: Proceedings of POPL 2013. ACM (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Claessen, K., Johansson, M., Rosén, D., Smallbone, N. (2013). Automating Inductive Proofs Using Theory Exploration. In: Bonacina, M.P. (eds) Automated Deduction – CADE-24. CADE 2013. Lecture Notes in Computer Science(), vol 7898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38574-2_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-38574-2_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38573-5
Online ISBN: 978-3-642-38574-2
eBook Packages: Computer ScienceComputer Science (R0)