• 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. Machine-checked proofs are becoming ever-larger, 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 general-purpose 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 sanity-checks 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 type-checking 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 ... assume-guarantee proof rule for carrying out compositional model checking on the types. Open simulation...
  • VeriSmall

  • Referenced in 6 articles [sw09788]
  • program, an end-to-end machine-checked 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, Proof-based ... reduction, SAT-based 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 light-weight ... compositional specification-based 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 low-cost 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 ... semi-interactive development of machine-checked 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, machine-checked verification of the seL4 microkernel from an abstract ... knowledge, this is the first formal proof of functional correctness of a complete, general-purpose...
  • 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]
  • Boyer-Moore logic, and the proof is mechanically checked with the Boyer-Moore theorem prover...
  • Isabelle/UTP

  • Referenced in 14 articles [sw21184]
  • host-logic 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...