seL4
From MaRDI portal
SeL4
Cited in
(only showing first 100 items - show all)- Comprehending Isabelle/HOL’s Consistency
- Formal reasoning under cached address translation
- Formal verification of integrity-preserving countermeasures against cache storage side-channels
- CoCon: a conference management system with formally verified document confidentiality
- The future of logic: foundation-independence
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Machine-checked mathematics
- Connecting higher-order separation logic to a first-order outside world
- Towards Formal Proof Script Refactoring
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Checking the Conformance of a Promela Design to its Formal Specification in Event-B
- Verified characteristic formulae for CakeML
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Mechanized metatheory revisited
- Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
- Eisbach: a proof method language for Isabelle
- Proof checking and logic programming
- Foreword to the special focus on formal proofs for mathematics and computer science
- A framework for the verification of certifying computations
- Proof checking and logic programming
- A formal proof of the Kepler conjecture
- Deep network guided proof search
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- Verified analysis of list update algorithms
- Machine assisted proof of ARMv7 instruction level isolation properties
- Refinement through restraint: bringing down the cost of verification
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- System-level non-interference of constant-time cryptography. I: Model
- Automated proof of Bell-LaPadula security properties
- Hoare-style logic for unstructured programs
- Concerned with the unprivileged: user programs in kernel refinement
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- Automated Certification of Implicit Induction Proofs
- Reasoning about Translation Lookaside Buffers
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- Trace-based verification of imperative programs with I/O
- 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
- Cogent
- HALO
- Matrix Operations
- ARMor
- AUSPICE-R
- Coverity
- Caper
- Infer
- Lifting
- Delphin
- CertiKOS
- BoogiePL
- Complx
This page was built for software: seL4
