swMATH9517MaRDI QIDQ21498FDOQ21498
Author name not available (Why is that?)
Official website: http://vst.cs.princeton.edu/
Cited In (only showing first 100 items - show all)
- Verifying Whiley programs with Boogie
- 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
- On models of higher-order separation logic
- A certificate infrastructure for machine-checked proofs of conditional information flow
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
- Verified characteristic formulae for CakeML
- The essence of higher-order concurrent separation logic
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Program logics for certified compilers
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Towards a unified theory of operational and axiomatic semantics
- From hoare logic to matching logic reachability
- Concise read-only specifications for better synthesis of programs with pointers
- Local reasoning for global graph properties
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Effect algebras, Girard quantales and complementation in separation logic
- Title not available (Why is that?)
- Chalice
- VeriFast
- CompCert
- HIP
- SLAyer
- Smallfoot
- NaCl
- PLT Redex
- VeriCool
- VeriSmall
- Viper
- VerCors
- Mtac
- ModuRes
- TweetNaCl
- Vellvm
- VeriML
- TCB
- Mezzo
- CoDeSe
- libclang
- AUTO2
- Verified software toolchain (invited talk)
- 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
- HACL*
- Nagini
- From rewriting logic, to programming language semantics, to program verification
- Formally verifying exceptions for low-level code with separation logic
- Whiley
- HolPy
- Relational decomposition
- JMLAutoTest
- RustBelt
- Whiteoak
- Abstraction and subsumption in modular verification of C programs
- A formal C memory model for separation logic
- Towards patterns for heaps and imperative lambdas
- LambdaMu-calculus
- VST-Floyd: a separation logic tool to verify correctness of C programs
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- KtoIsabelle
- CBench
- RHLE Benchmarks
- Connecting higher-order separation logic to a first-order outside world
- Safe functional systems through integrity types and verified assembly
- Transfinite step-indexing: decoupling concrete and logical steps
- Bringing Order to the Separation Logic Jungle
- MoSeL
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
This page was built for software: Toolchain
