seL4
From MaRDI portal
SeL4
Cited in
(only showing first 100 items - show all)- A synthesis of the procedural and declarative styles of interactive theorem proving
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- ACL2
- JMLUnit
- GeneSyst
- Isabelle/HOL
- MizarMode
- RAISE
- Isabelle/jEdit
- PIDE
- HOL-Omega
- Limmat
- Rodin
- VCC
- CompCertTSO
- LCF
- CakeML
- FABRIK
- CERES
- CertiCrypt
- TRX
- DESUMA
- GIDDES
- CompCert
- Toolchain
- PhoX
- VeriSmall
- Paco
- Nighthawk
- SPARK Pro
- Poly/ML
- Coquelicot
- Locales
- BAP
- Ynot
- Eisbach
- Mtac
- ConfiChair
- Rtac
- QuickChick
- FreeRTOS
- Vellvm
- VeriML
- TCT
- Yampa
- CodeSonar
- Jif
- Klockwork
- NAT2TEST
- CoSMed
- EXPLODE
- Ur/Web
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- Cogent
- HALO
- Matrix Operations
- ARMor
- AUSPICE-R
- Coverity
- Caper
- Infer
- Lifting
- Delphin
- CertiKOS
- BoogiePL
- Complx
- Transfer
- Teyjus
- CertiCoq
- Charge!
- CSimpl
- EROS
- GRASShopper
- kepler98
- ModelPlex
- GitLab
- DeltaJ
- JBMC
- DarwinSPL
- DeltaEcore
- Klocwork
- JOANA
- SCCharts
- SCEst
- Gallina
- Coinductive
- Cayley-Hamilton
- Echelon Form
- Barrelfish
- Gauss-Jordan
- Graph Theory
- CAVA LTL Modelchecker
- Kami
- QR Decomposition
- List Update Algorithms
- Piton
- Jinja not Java
- Tame Graphs
- Rank Nullity
This page was built for software: seL4
