- Referenced in 11 articles
- overall aim is to connect LCF-style provers like Isabelle...
- Referenced in 8 articles
- metaphor suited to visualize the LCF-style prover design, and a methodology for the implementation...
- Referenced in 5 articles
- based on sequent calculus with an LCF-style architecture. Psyche is a modular proof-search...
- Referenced in 3 articles
- results. Detailed performance data shows that LCF-style certificate checking is feasible even for large...
- Referenced in 291 articles
- ACL2 is both a programming language in which...
- Referenced in 719 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 584 articles
- An extensible SAT-solver. MiniSat is a minimalistic...
- Referenced in 524 articles
- ML (’Meta Language’) is a general-purpose functional...
- Referenced in 96 articles
- Building formal method tools in the Isabelle/Isar framework...
- Referenced in 59 articles
- SATLIB is a collection of benchmark problems, solvers...
- Referenced in 89 articles
- The KRAKATOA tool for certification of JAVA/JAVACARD programs...
- Referenced in 634 articles
- PVS is a verification system: that is, a...
- Referenced in 136 articles
- Why3 is a platform for deductive program verification...
- Referenced in 145 articles
- Theorem proving system supporting both interactive proof development...
- Referenced in 63 articles
- Caduceus used to be a verification tool for...
- Referenced in 37 articles
- zChaff is an implementation of the well known...
- Referenced in 594 articles
- Higher Order Logic (HOL) is a programming environment...