seL4

swMATH15222MaRDI QIDQ27113FDOQ27113

Author name not available (Why is that?)

Described by source

• Experience report

Cited In (86)

• Formal verification of integrity-preserving countermeasures against cache storage side-channels
• From a Proven Correct Microkernel to Trustworthy Large Systems
• Checking the Conformance of a Promela Design to its Formal Specification in Event-B
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• How Hard Is Positive Quantification?
• Connecting Higher-Order Separation Logic to a First-Order Outside World
• A Framework for the Automatic Formal Verification of Refinement from Cogent to C
• Title not available (Why is that?)
• Principled Software Development
• Fault-tolerant functional reactive programming (extended version)
• Title not available (Why is that?)
• Featherweight VeriFast
• How to make ad hoc proof automation less ad hoc
• Verified Analysis of List Update Algorithms.
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• Formal reasoning under cached address translation
• 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)
• Towards Formal Proof Script Refactoring
• CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Extensible and Efficient Automation Through Reflective Tactics
• Noninterference for Operating System Kernels
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Mechanized metatheory revisited
• AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
• Mtac: A monad for typed tactic programming in Coq
• Unifying Heterogeneous State-Spaces with Lenses
• Proof checking and logic programming
• Eisbach: a proof method language for Isabelle
• A framework for the verification of certifying computations
• Foreword to the special focus on formal proofs for mathematics and computer science
• Bar Induction is Compatible with Constructive Type Theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• One Logic to Use Them All
• Refinement through restraint: bringing down the cost of verification
• 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
• Automated Certification of Implicit Induction Proofs
• Verified Characteristic Formulae for CakeML
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
• Reasoning about Translation Lookaside Buffers
• HOL Zero’s Solutions for Pollack-Inconsistency
• Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
• Trace-based verification of imperative programs with I/O
• Mechanised Separation Algebra
• Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
• Trusting computations: a mechanized proof from partial differential equations to actual program
• CoSMed: a confidentiality-verified social media platform
• Introduction to ``Milestones in interactive theorem proving
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Toward compositional verification of interruptible OS kernels and device drivers
• Title not available (Why is that?)
• Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
• A learning-based fact selector for Isabelle/HOL
• Physical addressing on real hardware in Isabelle/HOL
• Program verification in the presence of cached address translation
• Model checking boot code from AWS data centers
• Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Using formal reasoning on a model of tasks for FreeRTOS
• ATP and presentation service for Mizar formalizations
• From LCF to Isabelle/HOL
• Pollack-inconsistency
• Computational logic: its origins and applications
• 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
• Proof tactics for assertions in separation logic
• SMT proof checking using a logical framework
• CoSMed: A Confidentiality-Verified Social Media Platform
• Proof Checking and Logic Programming
• Deep Network Guided Proof Search
• Priority inheritance protocol proved correct
• Challenges and Experiences in Managing Large-Scale Proofs
• More SPASS with Isabelle
• Formalization of Abstract State Transition Systems for SAT
• Beyond Provable Security Verifiable IND-CCA Security of OAEP
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• versat: A Verified Modern SAT Solver
• seL4 Enforces Integrity
• Comprehending Isabelle/HOL’s Consistency

This page was built for software: seL4