Isabelle/HOL
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Efficiently checking propositional refutations in HOL theorem provers
- On the correctness of upper layers of automotive systems
- Operating system verification---an overview
- Winskel is (almost) right: Towards a mechanized semantics textbook
- Apron
- ACL2
- Boolector
- Coq
- Dafny
- GCLC
- Grail
- HasCasl
- HOL-Boogie
- HYBRID
- ILTP
- Isabelle
- jETI
- KANT/KASH
- KeY-C
- LEO-II
- MetiTarski
- MiniSat
- binstretch
- PCM library
- finmap
- PyRes
- PAYNT
- Sequoia
- ROSMonitoring
- Marathon 2
- Nitpick
- Ott
- Proviola
- OCL2AC
- AMulet
- Goeland
- metalib
- FRAT
- Cubical Agda
- EasyUC
- solc-verify
- solgraph
- EthVer
- textX
- LGSVL
- ARQMath
- Wooki
- woot-haskell
- wootjs
- Woot
- BtorMC
- cake_lpr
- Nunchaku
- RelView
- jsCoq
- HolPy
- Q#
- simpA
- SUBSEXPL
- Theorema
- TkWinHOL
- TPS
- PRISM
- ML
- ALDOR
- Alloy
- Rapide
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- FocusCheck
- Cogent
- Prosper
- Verified bytecode subroutines
- Bytecode verification by model checking
- Beluga
- CLEAN
- IMP++
- veriSoft
- SecureUML
- TinkerType
- RuleML
- ArcAngel
- THINKER
- JavaFAN
- MizarMode
- SafeDpi
- CoqJVM
- Isabelle/Isar
- IsaPlanner
- AFRA
- FRACTRAN
- LARCH
- CASL
- TAPS
- MPTP
- TVOC
- MPTP 0.2
- VLISP
- IMPACT
- OTTER
- VAMPIRE
This page was built for software: Isabelle/HOL
