Cited in
(only showing first 100 items - show all)- QED reloaded: towards a pluralistic formal library of mathematical knowledge
- 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
- Model checking boot code from AWS data centers
- CSimpl: a rely-guarantee-based framework for verifying concurrent programs
- Beyond provable security verifiable IND-CCA security of OAEP
- 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
- CoSMed: a confidentiality-verified social media platform
- seL4 enforces integrity
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- TrABin
- Deep network guided proof search
- Eisbach: a proof method language for Isabelle
- Proof checking and logic programming
- Formalization of Abstract State Transition Systems for SAT
- From LCF to Isabelle/HOL
- Challenges and experiences in managing large-scale proofs
- Proof tactics for assertions in separation logic
- Proof checking and logic programming
- Pollack-inconsistency
- Using formal reasoning on a model of tasks for FreeRTOS
- ATP and presentation service for Mizar formalizations
- Automated proof of Bell-LaPadula security properties
- CoCon: a conference management system with formally verified document confidentiality
- Noninterference for operating system kernels
- Verified characteristic formulae for CakeML
- Hoare-style logic for unstructured programs
- Trace-based verification of imperative programs with I/O
- Concerned with the unprivileged: user programs in kernel refinement
- Mechanised Separation Algebra
- Comprehending Isabelle/HOL’s Consistency
- Bar induction is compatible with constructive type theory
- Coccinelle
- JSetL
- Maximum Cardinality Matching
- Cloc
- Isabelle/DOF
- CacheAudit
- JRIF
- IOzone
- ShortestPath
- SMT proof checking using a logical framework
- versat: A Verified Modern SAT Solver
- SETL
- HACL*
- FlowFox
- Pintos
- Xv6
- Automated Certification of Implicit Induction Proofs
- CoCon
- More SPASS with Isabelle
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- Mtac: a monad for typed tactic programming in Coq
- Mechanized metatheory revisited
- Towards Formal Proof Script Refactoring
- System-level non-interference of constant-time cryptography. I: Model
- One logic to use them all
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
- Texada
- A framework for the verification of certifying computations
- Foreword to the special focus on formal proofs for mathematics and computer science
- 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
- 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
- Unifying heterogeneous state-spaces with lenses
- HOL Zero's solutions for Pollack-inconsistency
- The future of logic: foundation-independence
- Machine assisted proof of ARMv7 instruction level isolation properties
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- Priority inheritance protocol proved correct
- Connecting higher-order separation logic to a first-order outside world
- 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
- scientific article; zbMATH DE number 7471719 (Why is no real title available?)
- Reasoning about Translation Lookaside Buffers
- The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- HolBA
- Formal reasoning under cached address translation
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- Checking the Conformance of a Promela Design to its Formal Specification in Event-B
- Extensible and efficient automation through reflective tactics
- Formal verification of integrity-preserving countermeasures against cache storage side-channels
- Verified analysis of list update algorithms
- Refinement through restraint: bringing down the cost of verification
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- How hard is positive quantification?
- Computational logic: its origins and applications
- From a proven correct microkernel to trustworthy large systems
- How to make ad hoc proof automation less ad hoc
- 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
- Machine-checked mathematics
- Fault-tolerant functional reactive programming (extended version)
- Featherweight VeriFast
This page was built for software: seL4
