Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala

doi:10.2168/LMCS-8(3:16)2012

Sylvain Conchon ; Evelyne Contejean ; Mohamed Iguernelala - Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

lmcs:1034 - Logical Methods in Computer Science, September 14, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:16)2012

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and ImplementationArticle

Authors: Sylvain Conchon ; Evelyne Contejean ; Mohamed Iguernelala

AC-completion efficiently handles equality modulo associative and commutative function symbols. When the input is ground, the procedure terminates and provides a decision algorithm for the word problem. In this paper, we present a modular extension of ground AC-completion for deciding formulas in the combination of the theory of equality with user-defined AC symbols, uninterpreted symbols and an arbitrary signature disjoint Shostak theory X. Our algorithm, called AC(X), is obtained by augmenting in a modular way ground AC-completion with the canonizer and solver present for the theory X. This integration rests on canonized rewriting, a new relation reminiscent to normalized rewriting, which integrates canonizers in rewriting steps. AC(X) is proved sound, complete and terminating, and is implemented to extend the core of the Alt-Ergo theorem prover.

Comment: 30 pages, full version of the paper TACAS'11 paper "Canonized Rewriting and Ground AC-Completion Modulo Shostak Theories" accepted for publication by LMCS (Logical Methods in Computer Science)

https://doi.org/10.2168/LMCS-8(3:16)2012

Source: arXiv.org:1207.3262

Volume: Volume 8, Issue 3

Secondary volumes: Selected Papers of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011)

Published on: September 14, 2012

Imported on: October 15, 2011

Keywords: Computer Science - Logic in Computer Science, F.4.1, G.4

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

10 Documents citing this article

Raphael Cohen;Eric Feron;Pierre-Loïc Garoche, 2020, Verification and Validation of Convex Optimization Algorithms for Model Predictive Control, arXiv (Cornell University), 17, 5, pp. 257-270, 10.2514/1.i010686, http://arxiv.org/abs/2005.12588.

Allan Blanchard;Frédéric Loulergue;Nikolai Kosmatov, 2019, Towards Full Proof Automation in Frama-C Using Auto-active Verification, Lecture notes in computer science, pp. 88-105, 10.1007/978-3-030-20652-9_6.

Maria Paola Bonacina;Pascal Fontaine;Christophe Ringeissen;Cesare Tinelli, 2019, Theory Combination: Beyond Equality Sharing, Open Repository and Bibliography (University of Liège), pp. 57-89, 10.1007/978-3-030-22102-7_3, https://orbi.uliege.be/handle/2268/256528.

Pierre Roux;Mohamed Iguernlala;Sylvain Conchon, 2018, A Non-linear Arithmetic Procedure for Control-Command Software Verification, Lecture notes in computer science, pp. 132-151, 10.1007/978-3-319-89963-3_8.

Raphael Cohen;Guillaume Davy;Eric Feron;Pierre-Loïc Garoche, 2017, Formal Verification for Embedded Implementation of Convex Optimization Algorithms, IFAC-PapersOnLine, 50, 1, pp. 5867-5874, 10.1016/j.ifacol.2017.08.1300, https://doi.org/10.1016/j.ifacol.2017.08.1300.

Sylvain Conchon;Mohamed Iguernlala;Alain Mebsout, 2017, AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo, Electronic Proceedings in Theoretical Computer Science, 239, pp. 1-13, 10.4204/eptcs.239.1, https://doi.org/10.4204/eptcs.239.1.

José Meseguer, 2016, Order-Sorted Rewriting and Congruence Closure, Lecture notes in computer science, pp. 493-509, 10.1007/978-3-662-49630-5_29.

Sylvain Conchon;Mohamed Iguernlala, 2016, Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo, Lecture notes in computer science, pp. 243-253, 10.1007/978-3-319-33951-1_18.

Sylvie Boldo, 2015, Formal Verification of Programs Computing the Floating-Point Average, Lecture notes in computer science, pp. 17-32, 10.1007/978-3-319-25423-4_2.

Sylvain Conchon;Mohamed Iguernelala, 2014, Tuning the Alt-Ergo SMT Solver for B Proof Obligations, Lecture notes in computer science, pp. 294-297, 10.1007/978-3-662-43652-3_27.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3211 times.

This article's PDF has been downloaded 452 times.