Verified Software Toolchain
From MaRDI portal
Publication:3000569
DOI10.1007/978-3-642-19718-5_1zbMath1326.68047MaRDI QIDQ3000569
Publication date: 19 May 2011
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-19718-5_1
68N01: General topics in the theory of software
Related Items
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers, Local Reasoning for Global Graph Properties, All-Path Reachability Logic, Formally-verified round-off error analysis of Runge-Kutta methods, A solver for arrays with concatenation, Efficient extensional binary tries, \textsf{LOGIC}: a Coq library for logics, RHLE: modular deductive verification of relational \(\forall \exists\) properties, The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, A complete semantics of \(\mathbb{K}\) and its translation to Isabelle, Reasoning about iteration and recursion uniformly based on big-step semantics, Safe functional systems through integrity types and verified assembly, From Rewriting Logic, to Programming Language Semantics, to Program Verification, Temporary Read-Only Permissions for Separation Logic, Verified Characteristic Formulae for CakeML, Relational Decomposition, AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
Uses Software
Cites Work
- Resources, concurrency, and local reasoning
- Formal verification of a C-like memory model and its uses for verifying program transformations
- A trustworthy proof checker
- A very modal model of a modern, major, general type system
- Local Reasoning for Storable Locks and Threads
- A theory of indirection via approximation
- Relaxed memory models
- Permission accounting in separation logic
- Foundational certified code in the Twelf metalogical framework
- Formal certification of a compiler back-end or
- Step-indexed kripke models over recursive worlds
- Oracle Semantics for Concurrent Separation Logic
- Logic for Programming, Artificial Intelligence, and Reasoning
