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

SYNASC, pp. 161-168, 2013.

Cited by: 9|Bibtex|Views7|Links
EI
Keywords:
smt, satisfiability modulo theories, non-linear arithmetic, ground completion modulo, interval analysisinterval analysissatisfiability modulo theories

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-li...More

Code:

Data:

Your rating :
0

 

Tags
Comments