Abstract
Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, ... are ubiquitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.
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.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
A. Bouhoula. Using induction and rewriting to verify and complete parameterized specifications. Theoretical Computer Science, 170, December 1996.
A. Bouhoula, E. Kounalis, M. Rusinowitch. Automated mathematical induction. Journal of Logic and Computation, 5(5):631–668, 1995.
A. Bouhoula, M. Rusinowitch. Implicit induction in conditional theories. Journal of Automated Reasoning, 14(2): 189–235, 1995.
R. S. Boyer, J. S. Moore. A Computational Logic Handbook. 1988.
R. Bündgen, W. Küchlin. Computing ground reducibility and inductively complete positions. In N. Dershowitz, editor, Rewriting Techniques and Applications, LNCS 355, pages 59–75, 1989.
J.R. Burch, E. M. Clarke, K.L. McMillan, D.L. Dill. Symbolic Model Checking: 1020 states and beyond. 5th Annual IEEE Symposium on Logic in Computer Science, pages 428–439, 1990.
D. Cyrluk, S. Rajan, N. Shankar, M. K. Srivas. Effective Theorem Proving for Hardware Verification. In K. Ramayya and K. Thomas, editors, Theorem Provers in Circuit Design LNCS 901, pages 203–222, 1994.
S. J. Garland, John V. Guttag. An overview of LP, the Larch Prover. In N. Dershowitz, editor, Rewriting Techniques and Applications, LNCS 355, pages 137–151, 1989.
J.-P. Jouannaud, E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82:1–33, 1989.
D. Kapur, P. Narendran, D. J. Rosenkrantz, H. Zhang. Sufficient completeness, ground-reducibility and their complexity. Acta Informatica, 28:311–350, 1991.
E. Kounalis M. Rusinowitch. Reasoning with conditional axioms. Annals of Mathematics and Artificial Intelligence, (15):125–149, 1995.
C. Marché. Réécriture modulo une théorie présentée par un système convergent et décidabilité du problème du mot dans certaines classes de théories équationnelles. Th. univ., Université de Paris-Sud (France), 1993.
S. Owre, J.M. Rushby, N. Shankar. A prototype verification system. In D. Kapur, editor, International Conference on Automated Deduction, LNAI 607, pages 748–752, 1992.
L. Pierre. An automatic generalisation method for the inductive proof of replicated and parallel architetures. In K. Ramayya and K. Thomas, editors, Theorem Provers in Circuit Design, LNCS 901, pages 72–91, 1994.
H. Zhang. Contextual rewriting in automated reasoning. Fundamenta Informaticae, (24):107–123, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berregeb, N., Bouhoula, A., Rusinowitch, M. (1996). Automated verification by induction with associative-commutative operators. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_71
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_71
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive