Verified software toolchain (invited talk)

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

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Recommendations

• VST-Floyd: a separation logic tool to verify correctness of C programs
• Verified squared, does critical software deserve verified tools?
• The verified software repository: a step towards the verifying compiler
• A Completely Verified Realistic Bootstrap Compiler
• A formally verified compiler back-end

Cites work

• A theory of indirection via approximation
• A trustworthy proof checker
• A very modal model of a modern, major, general type system
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Foundational certified code in the Twelf metalogical framework
• Local Reasoning for Storable Locks and Threads
• Logic for Programming, Artificial Intelligence, and Reasoning
• Oracle Semantics for Concurrent Separation Logic
• Permission accounting in separation logic
• Relaxed memory models
• Resources, concurrency, and local reasoning
• Step-indexed Kripke models over recursive worlds

Cited in

(23)

• Formally-verified round-off error analysis of Runge-Kutta methods
• 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
• A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Verified squared, does critical software deserve verified tools?
• The verified software repository: a step towards the verifying compiler
• A solver for arrays with concatenation
• Efficient extensional binary tries
• Verified characteristic formulae for CakeML
• Panellist position statement: some industrial experience with program verification
• AUSPICE-R: automatic safety-property proofs for realistic features in machine code
• RHLE: modular deductive verification of relational \(\forall \exists\) properties
• Safe functional systems through integrity types and verified assembly
• Reasoning about iteration and recursion uniformly based on big-step semantics
• \textsf{LOGIC}: a Coq library for logics
• Temporary read-only permissions for separation logic
• From rewriting logic, to programming language semantics, to program verification
• Concise read-only specifications for better synthesis of programs with pointers
• Local reasoning for global graph properties
• The Verified Software Initiative: A Manifesto
• Relational decomposition
• Balancing the load. Leveraging a semantics stack for systems verification

Describes a project that uses

Uses Software

• Toolchain
• TCB

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)