The following pages link to seL4 (Q27113):
Displaying 36 items.
- Verified Characteristic Formulae for CakeML (Q2988660) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- From a Proven Correct Microkernel to Trustworthy Large Systems (Q3067529) (← links)
- Beyond Provable Security Verifiable IND-CCA Security of OAEP (Q3073706) (← links)
- seL4 Enforces Integrity (Q3088017) (← links)
- Automated Certification of Implicit Induction Proofs (Q3100200) (← links)
- AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code (Q3179279) (← links)
- Unifying Heterogeneous State-Spaces with Lenses (Q3179407) (← links)
- Featherweight VeriFast (Q3196351) (← links)
- Formalization of Abstract State Transition Systems for SAT (Q3224685) (← links)
- CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs (Q3303910) (← links)
- Checking the Conformance of a Promela Design to its Formal Specification in Event-B (Q3460222) (← links)
- Principled Software Development (Q4558903) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- Verified Analysis of List Update Algorithms. (Q4636599) (← links)
- Deep Network Guided Proof Search (Q4645728) (← links)
- Reasoning about Translation Lookaside Buffers (Q4645755) (← links)
- Noninterference for Operating System Kernels (Q4916056) (← links)
- One Logic to Use Them All (Q4928425) (← links)
- (Q5028488) (← links)
- Connecting Higher-Order Separation Logic to a First-Order Outside World (Q5041105) (← links)
- Fault-tolerant functional reactive programming (extended version) (Q5120226) (← links)
- Pollack-inconsistency (Q5170237) (← links)
- How to make ad hoc proof automation less ad hoc (Q5176973) (← links)
- QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge (Q5195275) (← links)
- Towards Formal Proof Script Refactoring (Q5200123) (← links)
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem (Q5204803) (← links)
- (Q5219924) (← links)
- Bar Induction is Compatible with Constructive Type Theory (Q5244386) (← links)
- How Hard Is Positive Quantification? (Q5278190) (← links)
- A FORMAL PROOF OF THE KEPLER CONJECTURE (Q5280247) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- (Q5417200) (← links)
- Proof Checking and Logic Programming (Q5743582) (← links)
- (Q5875442) (← links)
- Characteristic formulae for liveness properties of non-terminating CakeML programs (Q5875446) (← links)
