• 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]
  • reflection-based 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 Fourier-Motzkin elimination; logic/Presburger.v: Presburger arithmetic and quantifier elimination; algebra_ext.v: Quantifier elimination...
  • ghc-typelits-presburger

  • Referenced in 1 article [sw26351]
  • typelits-presburger package. ghc-typelits-presburger: Presburger Arithmetic Solver for GHC Type-level 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 general-purpose 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...