Verified Software Toolchain

DOI10.1007/978-3-642-19718-5_1zbMath1326.68047OpenAlexW2213989452MaRDI QIDQ3000569

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)

Related Items

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle, Concise Read-Only Specifications for Better Synthesis of Programs with Pointers, Local Reasoning for Global Graph Properties, The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code, Reasoning about iteration and recursion uniformly based on big-step semantics, From Rewriting Logic, to Programming Language Semantics, to Program Verification, 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, Safe functional systems through integrity types and verified assembly, Temporary Read-Only Permissions for Separation Logic, Verified Characteristic Formulae for CakeML, All-Path Reachability Logic, Relational Decomposition

Uses Software

• Toolchain
• TCB

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