CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Bound Propagation for Arithmetic Reasoning in Vampire

Ioan Dragan ; Konstantin Korovin ; Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Andrei Voronkov
Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, September 23-26, 2013, Timisoara, Romania. Nikolaj Bjorner (editors), IEEE series p. 169-176. (2013)
[Konferensbidrag, refereegranskat]

This paper describes an implementation and experimental evaluation of a recently introduced bound propagation method for solving systems of linear inequalities over the reals and rationals. The implementation is part of the first-order theorem prover Vampire. The input problems are systems of linear inequalities over reals or rationals. Their satisfiability is checked by assigning values to the variables of the system and propagating the bounds on these variables. To make the method efficient, we use various strategies for representing numbers, selecting variable orderings, choosing variable values and propagating bounds. We evaluate our implementation on a large number of examples and compare it with state-of-the-art SMT solvers.

Nyckelord: formal methods, theorem proving, automated reasoning, Arithmetic reasoning; Bound propagation method; Conflict resolution; Linear arithmetic; Linear real arithmetic


Article number 6821147



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-01-09. Senast ändrad 2016-08-22.
CPL Pubid: 192005

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)