seL4
From MaRDI portal
SeL4
Cited in
(only showing first 100 items - show all)- ACL2
- JMLUnit
- Texada
- GeneSyst
- Isabelle/HOL
- MizarMode
- RAISE
- Introduction to ``Milestones in interactive theorem proving
- The role of the Mizar mathematical library for interactive proof development in Mizar
- CoSMed: a confidentiality-verified social media platform
- Toward compositional verification of interruptible OS kernels and device drivers
- Proof tactics for assertions in separation logic
- Physical addressing on real hardware in Isabelle/HOL
- Program verification in the presence of cached address translation
- PIDE
- Isabelle/jEdit
- HOL-Omega
- Limmat
- Rodin
- VCC
- ATP and presentation service for Mizar formalizations
- Foreword to the special focus on formal proofs for mathematics and computer science
- CompCertTSO
- CoCon: a conference management system with formally verified document confidentiality
- Automated proof of Bell-LaPadula security properties
- LCF
- Hoare-style logic for unstructured programs
- Model checking boot code from AWS data centers
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- An automatically verified prototype of the Tokeneer ID station specification
- Experiences from exporting major proof assistant libraries
- CakeML
- TRX
- FABRIK
- CERES
- CertiCrypt
- Toolchain
- DESUMA
- GIDDES
- CompCert
- VeriSmall
- PhoX
- Formal reasoning under cached address translation
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- SPARK Pro
- From LCF to Isabelle/HOL
- Paco
- Nighthawk
- Priority inheritance protocol proved correct
- Mechanized metatheory revisited
- Formal verification of integrity-preserving countermeasures against cache storage side-channels
- Poly/ML
- Coquelicot
- A framework for the verification of certifying computations
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Trusting computations: a mechanized proof from partial differential equations to actual program
- System-level non-interference of constant-time cryptography. I: Model
- Ynot
- Locales
- SMT proof checking using a logical framework
- BAP
- Mtac
- Eisbach
- Rtac
- ConfiChair
- QuickChick
- Vellvm
- VeriML
- TCT
- Yampa
- FreeRTOS
- Proof checking and logic programming
- The future of logic: foundation-independence
- Extensible and efficient automation through reflective tactics
- HOL Zero's solutions for Pollack-inconsistency
- CoSMed: a confidentiality-verified social media platform
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- Jif
- CodeSonar
- Klockwork
- NAT2TEST
- Eisbach: a proof method language for Isabelle
- A synthesis of the procedural and declarative styles of interactive theorem proving
- versat: A Verified Modern SAT Solver
- Challenges and experiences in managing large-scale proofs
- Mechanised Separation Algebra
- More SPASS with Isabelle
- EXPLODE
- CoSMed
- Ur/Web
- Machine assisted proof of ARMv7 instruction level isolation properties
- Refinement through restraint: bringing down the cost of verification
- Machine-checked mathematics
- Verified characteristic formulae for CakeML
- Comprehending Isabelle/HOL’s Consistency
- AUSPICE-R
- ARMor
- Cogent
- From a proven correct microkernel to trustworthy large systems
This page was built for software: seL4
