Verified software toolchain (invited talk)
From MaRDI portal
Publication:3000569
DOI10.1007/978-3-642-19718-5_1zbMATH Open1326.68047OpenAlexW2213989452MaRDI QIDQ3000569FDOQ3000569
Authors: Andrew W. Appel 
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
Recommendations
Cites Work
- A trustworthy proof checker
- Local Reasoning for Storable Locks and Threads
- Permission accounting in separation logic
- Resources, concurrency, and local reasoning
- Step-indexed Kripke models over recursive worlds
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- A very modal model of a modern, major, general type system
- Relaxed memory models
- Logic for Programming, Artificial Intelligence, and Reasoning
- Oracle Semantics for Concurrent Separation Logic
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Foundational certified code in the Twelf metalogical framework
- A theory of indirection via approximation
Cited In (23)
- Reasoning about iteration and recursion uniformly based on big-step semantics
- \textsf{LOGIC}: a Coq library for logics
- Safe functional systems through integrity types and verified assembly
- Balancing the load. Leveraging a semantics stack for systems verification
- Formally-verified round-off error analysis of Runge-Kutta methods
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
- Verified characteristic formulae for CakeML
- A solver for arrays with concatenation
- Efficient extensional binary tries
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Concise read-only specifications for better synthesis of programs with pointers
- Local reasoning for global graph properties
- RHLE: modular deductive verification of relational \(\forall \exists\) properties
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
- Verified squared, does critical software deserve verified tools?
- The Verified Software Initiative: A Manifesto
- Panellist position statement: some industrial experience with program verification
- Temporary read-only permissions for separation logic
- From rewriting logic, to programming language semantics, to program verification
- The verified software repository: a step towards the verifying compiler
- Relational decomposition
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
Uses Software
This page was built for publication: Verified software toolchain (invited talk)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000569)
