
VAMPIRE
 Referenced in 258 articles
[sw02918]
 used to accelerate some costly operations, e.g., checks of ordering constraints. Although the kernel ... proved, the system produces a verifiable proof, which validates both the clausification phase...

Eisbach
 Referenced in 8 articles
[sw13077]
 Isabelle proof method language. Machinechecked proofs are becoming everlarger, presenting an increasing maintenance...

FoCaLiZe
 Referenced in 10 articles
[sw12384]
 proof assistant to check the proofs, a source file for the OCaml compiler to build...

TLAPS
 Referenced in 9 articles
[sw09528]
 Proof System (TLAPS) mechanically checks TLA+ proofs. TLA+ is a generalpurpose formal specification language ... describing concurrent and distributed systems. The TLA+ proof language is declarative, hierarchical, and scalable ... easily checked by hand is needed for safety.) For examples, see the proof...

Ott
 Referenced in 31 articles
[sw00663]
 mathematics or the formal mathematics of a proof assistant  make it much harder than necessary ... that sanitychecks such definitions and compiles them into proof assistant code...

HySAT
 Referenced in 25 articles
[sw01980]
 HySAT: An efficient proof engine for bounded model checking of hybrid systems n this paper...

PolyTOIL
 Referenced in 23 articles
[sw14205]
 formal definition of typechecking rules and semantics. A proof of type safety is obtained...

PIPER
 Referenced in 28 articles
[sw11478]
 fundamental issues in making model checking viable for software. This paper proposes new techniques ... assumeguarantee proof rule for carrying out compositional model checking on the types. Open simulation...

VeriSmall
 Referenced in 6 articles
[sw09788]
 program, an endtoend machinechecked proof guarantees that the assembly language...

DiVer
 Referenced in 10 articles
[sw01938]
 Model Checking (BMC) and Distributed BMC over a network of workstations for falsification, Proofbased ... reduction, SATbased Unbounded Model Checking and Induction for proofs, Efficient Memory Modeling...

Ivy
 Referenced in 9 articles
[sw41668]
 algorithms, supporting modular specification, implementation and proof. Ivy supports proving safety and liveness properties ... solver, abstraction and model checking, and manual proofs using natural deduction. It supports lightweight ... compositional specificationbased testing and bounded model checking. Ivy can extract executable distributed programs ... support decidable automated reasoning, to improve proof stability and to provide transparency in the case...

FLASH
 Referenced in 46 articles
[sw02233]
 that allow signatures to be computed and checked by a lowcost smart card ... security is controversial, since we have no proof of security, but the best known attacks...

CoqJVM
 Referenced in 4 articles
[sw02002]
 formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms ... semiinteractive development of machinechecked proofs. Typical applications include the formalization of programming languages...

Bedwyr
 Referenced in 22 articles
[sw09460]
 generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings ... recent advances in the theory of proof search. The first is centered on the fact ... result, proof search in such a sequent calculus can capture simple model checking problems...

TAME
 Referenced in 5 articles
[sw28703]
 used both to mechanically check hand proofs in a straightforward way and to create proof...

seL4
 Referenced in 90 articles
[sw15222]
 experience in performing the formal, machinechecked verification of the seL4 microkernel from an abstract ... knowledge, this is the first formal proof of functional correctness of a complete, generalpurpose...

mathlib
 Referenced in 3 articles
[sw36839]
 tools for the library which check proof developments for subtle mistakes in the code...

Kit
 Referenced in 7 articles
[sw22321]
 BoyerMoore logic, and the proof is mechanically checked with the BoyerMoore theorem prover...

Isabelle/UTP
 Referenced in 14 articles
[sw21184]
 hostlogic type checking that subsumes the need for typing proof obligations in the object...

Skeptik
 Referenced in 6 articles
[sw11917]
 introduces Skeptik: a system for checking, compressing and improving proofs obtained...