seL4
From MaRDI portal
Software:27113
No author found.
Related Items (86)
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving ⋮ How Hard Is Positive Quantification? ⋮ Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm ⋮ A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Connecting Higher-Order Separation Logic to a First-Order Outside World ⋮ versat: A Verified Modern SAT Solver ⋮ Eisbach: a proof method language for Isabelle ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Verified Analysis of List Update Algorithms. ⋮ Unnamed Item ⋮ Proof checking and logic programming ⋮ Challenges and Experiences in Managing Large-Scale Proofs ⋮ AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Checking the Conformance of a Promela Design to its Formal Specification in Event-B ⋮ Mechanised Separation Algebra ⋮ More SPASS with Isabelle ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Principled Software Development ⋮ Computational logic: its origins and applications ⋮ Unnamed Item ⋮ Featherweight VeriFast ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ 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 ⋮ Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties ⋮ System-level non-interference of constant-time cryptography. I: Model ⋮ Formalization of Abstract State Transition Systems for SAT ⋮ Trace-based verification of imperative programs with I/O ⋮ Proof tactics for assertions in separation logic ⋮ Unnamed Item ⋮ Using formal reasoning on a model of tasks for FreeRTOS ⋮ ATP and presentation service for Mizar formalizations ⋮ Fault-tolerant functional reactive programming (extended version) ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Formal reasoning under cached address translation ⋮ SMT proof checking using a logical framework ⋮ Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning ⋮ Refinement through restraint: bringing down the cost of verification ⋮ Verified Characteristic Formulae for CakeML ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ Unnamed Item ⋮ Predicate extension of symbolic memory graphs for the analysis of memory safety correctness ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs ⋮ Deep Network Guided Proof Search ⋮ Reasoning about Translation Lookaside Buffers ⋮ Noninterference for Operating System Kernels ⋮ Pollack-inconsistency ⋮ How to make ad hoc proof automation less ad hoc ⋮ One Logic to Use Them All ⋮ Proof Checking and Logic Programming ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ From LCF to Isabelle/HOL ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ Automated proof of Bell-LaPadula security properties ⋮ Towards Formal Proof Script Refactoring ⋮ Physical addressing on real hardware in Isabelle/HOL ⋮ Program verification in the presence of cached address translation ⋮ From a Proven Correct Microkernel to Trustworthy Large Systems ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Hoare-style logic for unstructured programs ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Concerned with the unprivileged: user programs in kernel refinement ⋮ Beyond Provable Security Verifiable IND-CCA Security of OAEP ⋮ Model checking boot code from AWS data centers ⋮ Priority inheritance protocol proved correct ⋮ seL4 Enforces Integrity ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM ⋮ HOL Zero’s Solutions for Pollack-Inconsistency ⋮ CoSMed: A Confidentiality-Verified Social Media Platform ⋮ A Framework for the Automatic Formal Verification of Refinement from Cogent to C ⋮ Automated Certification of Implicit Induction Proofs ⋮ An automatically verified prototype of the Tokeneer ID station specification ⋮ Experiences from exporting major proof assistant libraries ⋮ Mechanized metatheory revisited ⋮ Formal verification of integrity-preserving countermeasures against cache storage side-channels ⋮ Bar Induction is Compatible with Constructive Type Theory ⋮ Unnamed Item ⋮ QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge ⋮ A framework for the verification of certifying computations ⋮ The future of logic: foundation-independence
This page was built for software: seL4
