The following pages link to seL4 (Q27113):
Displayed 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (Q333325) (← links)
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (Q457250) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Concerned with the unprivileged: user programs in kernel refinement (Q736848) (← links)
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) (Q832157) (← links)
- Using formal reasoning on a model of tasks for FreeRTOS (Q903515) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- Toward compositional verification of interruptible OS kernels and device drivers (Q1663225) (← links)
- Proof tactics for assertions in separation logic (Q1687747) (← links)
- Physical addressing on real hardware in Isabelle/HOL (Q1791136) (← links)
- Program verification in the presence of cached address translation (Q1791200) (← links)
- ATP and presentation service for Mizar formalizations (Q1945905) (← links)
- Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
- CoCon: a conference management system with formally verified document confidentiality (Q2031419) (← links)
- Automated proof of Bell-LaPadula security properties (Q2031424) (← links)
- Hoare-style logic for unstructured programs (Q2038040) (← links)
- Model checking boot code from AWS data centers (Q2050104) (← links)
- Integration of formal proof into unified assurance cases with Isabelle/SACM (Q2065527) (← links)
- An automatically verified prototype of the Tokeneer ID station specification (Q2069869) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Formal reasoning under cached address translation (Q2209539) (← links)
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness (Q2226974) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Priority inheritance protocol proved correct (Q2303234) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formal verification of integrity-preserving countermeasures against cache storage side-channels (Q2324198) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm (Q2360828) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
- System-level non-interference of constant-time cryptography. I: Model (Q2417947) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Proof checking and logic programming (Q2628296) (← links)
- Extensible and Efficient Automation Through Reflective Tactics (Q2802496) (← links)
- HOL Zero’s Solutions for Pollack-Inconsistency (Q2829240) (← links)
- CoSMed: A Confidentiality-Verified Social Media Platform (Q2829248) (← links)
- A Framework for the Automatic Formal Verification of Refinement from Cogent to C (Q2829268) (← links)
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving (Q2881098) (← links)
- versat: A Verified Modern SAT Solver (Q2891429) (← links)
- Challenges and Experiences in Managing Large-Scale Proofs (Q2907311) (← links)
- Mechanised Separation Algebra (Q2914753) (← links)
- More SPASS with Isabelle (Q2914754) (← links)
- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties (Q2938055) (← links)
- Refinement through restraint: bringing down the cost of verification (Q2982005) (← links)
- (Q2988059) (← links)