Archive of Formal Proofs
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Adapting functional programs to higher order logic
- Operating system verification---an overview
- ACL2
- Coq
- DDDLIB
- HOL-Boogie
- Isabelle
- LEO-II
- Roosterize
- PCM library
- PyRes
- Sequoia
- ROSMonitoring
- Nitpick
- metalib
- EasyUC
- solc-verify
- Wooki
- woot-haskell
- wootjs
- Woot
- Nunchaku
- RelView
- TkWinHOL
- APS-1
- ML
- Rapide
- Prosper
- Isabelle/HOL
- RuleML
- THINKER
- CoqJVM
- Isabelle/Isar
- AFRA
- SQEMA
- CoqEAL
- MathWebSearch
- SMART_
- Algolib
- TLA
- The role of the Mizar mathematical library for interactive proof development in Mizar
- A verified ODE solver and the Lorenz attractor
- Verified iptables firewall analysis and verification
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Formalization of the resolution calculus for first-order logic
- Isar
- Mizar
- Markov chains and Markov decision processes in Isabelle/HOL
- The matrix reproved (verification pearl)
- Isabelle/ZF
- The flow of ODEs: formalization of variational equation and Poincaré map
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Growth of normalizing sequences in limit theorems for conservative maps
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Netsoft
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- Refinement to imperative HOL
- HOL
- An algebraic framework for minimum spanning tree problems
- Tarski geometry axioms. III
- CIRC
- ETPS
- ClawZ
- AEtnaNova
- PIDE
- Isabelle/jEdit
- HOL Light
- HOL-Omega
- CeTA
- Satallax
- MUSCADET
- Sledgehammer
- HOCL
- Isabelle/PIDE
- veriT
- NQTHM
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- Verifying minimum spanning tree algorithms with Stone relation algebras
- (Co)inductive proof systems for compositional proofs in reachability logic
- Unifying theories of reactive design contracts
- Formalization of the Poincaré disc model of hyperbolic geometry
- \(\mathrm{HO}\pi\) in Coq
- CoCon: a conference management system with formally verified document confidentiality
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
- LCF
- CLSAT
- versat
- Automated verification of reactive and concurrent programs by calculation
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- ForMaRE
- CakeML
- TRX
- A formally verified, optimized monitor for metric first-order dynamic logic
- Formalizing a Seligman-style tableau system for hybrid logic (short paper)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- A formalization of Dedekind domains and class groups of global fields
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- A formalization of the Smith normal form in higher-order logic
This page was built for software: Archive of Formal Proofs
