A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo

Author

Conchon, Sylvain ; Iguernelala, Mohamed ; Mebsout, Alain

Author_Institution

LRI, Univ. Paris-Sud, Orsay, France

fYear

2013

fDate

23-26 Sept. 2013

Firstpage

161

Lastpage

168

Abstract

In this paper, we describe a collaborative framework for reasoning modulo simple properties of non-linear integer arithmetic. This framework relies on the AC(X) combination method and on interval calculus. The first component is used to handle equalities of linear integer arithmetic and associativity and commutativity properties of non-linear multiplication. The interval calculus component is used - in addition to standard linear operations over inequalities - to refine bounds of non-linear terms and to inform the SAT solver about judicious case-splits on bounded intervals. The framework has been implemented in the Alt-Ergo theorem prover. We show its effectiveness on a set of formulas generated from deductive program verification.

Keywords

arithmetic; computability; groupware; inference mechanisms; integration; mathematics computing; program verification; theorem proving; AC(X) combination method; Alt-Ergo theorem prover; SAT solver; associativity properties; bounded intervals; collaborative framework; commutativity properties; deductive program verification; interval calculus component; judicious case-splits; linear integer arithmetic; linear operations; modulo simple properties; nonlinear integer arithmetic reasoning; nonlinear multiplication; Calculus; Cognition; Collaboration; Context; Equations; Inference algorithms; Standards; ground completion modulo; interval analysis; non-linear arithmetic; satisfiability modulo theories; smt;

fLanguage

English

Publisher

ieee

Conference_Titel

Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2013 15th International Symposium on

Conference_Location

Timisoara

Print_ISBN

978-1-4799-3035-7

Type

conf

DOI

10.1109/SYNASC.2013.29

Filename

6821146