Toolchain

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