1996 | ReviewPaper | Chapter
Automated verification by induction with associative-commutative operators
Authors : Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.