
Rast
 Referenced in 1 article
[sw41190]
 Presburger arithmetic with a few significant optimizations, and a heuristic extension to nonlinear constraints. Rast...

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

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

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

polymake
 Referenced in 328 articles
[sw00724]
 polymake is open source software for research in...

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

Kronos
 Referenced in 274 articles
[sw01270]
 KRONOS is a tool developed with the aim...

TREX
 Referenced in 47 articles
[sw01388]
 TREX is a tool for automatic analysis of...

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

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

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

Uppaal
 Referenced in 658 articles
[sw04702]
 Uppaal is an integrated tool environment for modeling...

z3
 Referenced in 606 articles
[sw04887]
 Z3 is a highperformance theorem prover being...

ARMC
 Referenced in 28 articles
[sw04949]
 ARMC: The Logical Choice for Software Model Checking...

Aspic
 Referenced in 24 articles
[sw04954]
 Combining widening and acceleration in linear relation analysis...

HOL
 Referenced in 594 articles
[sw05492]
 Higher Order Logic (HOL) is a programming environment...

MONA
 Referenced in 135 articles
[sw06170]
 MONA implementation secrets. The MONA tool provides an...

Princess
 Referenced in 28 articles
[sw06872]
 Theorem Proving in FirstOrder Logic modulo Linear...

BPEL2oWFN
 Referenced in 28 articles
[sw06956]
 GNU BPEL2oWFN translates a web service expressed in...