
Princess
 Referenced in 23 articles
[sw06872]
 Princess is a theorem prover for Presburger arithmetic with uninterpreted predicates. This means that Princess...

Presburger Automata
 Referenced in 9 articles
[sw28603]
 reflectionbased decision procedure for Presburger arithmetic, which is efficiently executable thanks to Isabelle...

TaPAS
 Referenced in 8 articles
[sw07286]
 TaPAS: the talence Presburger arithmetic suite. TaPAS is a suite of libraries dedicated ... like library SaTAF used for encoding Presburger formulae to automata, and (3) the very first...

Eldarica
 Referenced in 2 articles
[sw09748]
 graphs whose edges are annotated by Presburger arithmetic formulas. We present Flata and Eldarica ... sound and complete interpolating prover for Presburger arithmetic. Both systems can solve several examples...

TERMINATOR
 Referenced in 3 articles
[sw06692]
 analyzing termination are based on Presburger arithmetic or linear programming, so they are valid only...

Omega++
 Referenced in 1 article
[sw32372]
 prove that adding infinities to Presburger arithmetic enables these improvements without sacrificing decidability. We develop ... certified decision procedure for Presburger arithmetic with infinity and benchmark its performance. Both the program...

Vass
 Referenced in 1 article
[sw34696]
 arithmetic and FourierMotzkin elimination; logic/Presburger.v: Presburger arithmetic and quantifier elimination; algebra_ext.v: Quantifier elimination...

ghctypelitspresburger
 Referenced in 1 article
[sw26351]
 typelitspresburger package. ghctypelitspresburger: Presburger Arithmetic Solver for GHC Typelevel natural numbers...

Coq
 Referenced in 1758 articles
[sw00161]
 Coq is a formal proof management system. It...

Macaulay2
 Referenced in 1585 articles
[sw00537]
 Macaulay2 is a software system devoted to supporting...

ManySAT
 Referenced in 31 articles
[sw00544]
 ManySAT: a parallel SAT solver. ManySAT, a new...

Normaliz
 Referenced in 146 articles
[sw00630]
 Normaliz is a tool for computations in affine...

ML
 Referenced in 502 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

ASTRAL
 Referenced in 17 articles
[sw02878]
 Hardware specification using the assertion language ASTRAL We...

VAMPIRE
 Referenced in 232 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem...

PVS
 Referenced in 603 articles
[sw03484]
 PVS is a verification system: that is, a...

HyTech
 Referenced in 321 articles
[sw04125]
 HyTech is an automatic tool for the analysis...

FLATA
 Referenced in 15 articles
[sw04142]
 FLATA is a toolset for the manipulation and...

UCLID
 Referenced in 25 articles
[sw04657]
 UCLID (pronounced ”Euclid”) is a tool for analyzing...