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

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

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

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
• 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
• A solver for arrays with concatenation
• Efficient extensional binary tries
• AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• 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 Characteristic Formulae for CakeML
• The Verified Software Initiative: A Manifesto
• Panellist position statement: some industrial experience with program verification
• The verified software repository: a step towards the verifying compiler
• Relational decomposition
• All-Path Reachability Logic
• Temporary Read-Only Permissions for Separation Logic
• Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
• Local Reasoning for Global Graph Properties
• From Rewriting Logic, to Programming Language Semantics, to Program Verification

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)