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