Cited in
(only showing first 100 items - show all)- KtoIsabelle
- CBench
- RHLE Benchmarks
- Connecting higher-order separation logic to a first-order outside world
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
- Extensible and efficient automation through reflective tactics
- MoSeL
- Safe functional systems through integrity types and verified assembly
- Transfinite step-indexing: decoupling concrete and logical steps
- LambdaMu-calculus
- Featherweight VeriFast
- Bringing Order to the Separation Logic Jungle
- Abstraction and subsumption in modular verification of C programs
- Verified software toolchain (invited talk)
- A formal C memory model for separation logic
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Verified cryptographic code for everybody
- A certificate infrastructure for machine-checked proofs of conditional information flow
- Towards patterns for heaps and imperative lambdas
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Verified characteristic formulae for CakeML
- The essence of higher-order concurrent separation logic
- Towards a unified theory of operational and axiomatic semantics
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- From hoare logic to matching logic reachability
- JMLUnit
- Chalice
- VeriFast
- CompCert
- HIP
- SLAyer
- Smallfoot
- NaCl
- PLT Redex
- VeriCool
- VeriSmall
- Viper
- VerCors
- Mtac
- ModuRes
- TweetNaCl
- Vellvm
- VeriML
- TCB
- Mezzo
- CoDeSe
- libclang
- AUTO2
- Formally verifying exceptions for low-level code with separation logic
- HALO
- ARMor
- AUSPICE-R
- K-Java
- KJS
- Caper
- Infer
- Verasco
- Fiat
- CertiKOS
- GRAT
- VACID-0
- CertiCoq
- Charge!
- Flicker
- CSimpl
- GRASShopper
- AstraVer
- Gallina
- Bedrock
- Edmonds-Karp
- Guardol
- Rust
- Kami
- Slide
- VST-Floyd
- Knuth Morris Pratt
- CacheAudit
- IEEE_Floating_Point
- Java+ITP
- K Prover
- Temporary read-only permissions for separation logic
- From rewriting logic, to programming language semantics, to program verification
- HACL*
- Nagini
- Concise read-only specifications for better synthesis of programs with pointers
- Local reasoning for global graph properties
- Program logics for certified compilers
- Verifying Whiley programs with Boogie
- Whiley
- HolPy
- JMLAutoTest
- RustBelt
- Whiteoak
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Effect algebras, Girard quantales and complementation in separation logic
- VST-Floyd: a separation logic tool to verify correctness of C programs
This page was built for software: Toolchain
