Verified software units

DOI10.1007/978-3-030-72019-3_5zbMATH Open1473.68035OpenAlexW3136796399MaRDI QIDQ2233451FDOQ2233451

Authors Lennart Beringer

Publication date 18 October 2021

Full work available at URL https://doi.org/10.1007/978-3-030-72019-3_5

zbMATH Keywords

positive subtypingabstract predicate declarationresidual predicateverified software toolchainverified software unit

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Abstraction and subsumption in modular verification of C programs
• Compositional CompCert
• scientific article; zbMATH DE number 140003
• Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
• Sound modular verification of C code executing in an unverified context

Cites work

• scientific article; zbMATH DE number 1670750 (Why is no real title available?)
• scientific article; zbMATH DE number 1006119 (Why is no real title available?)
• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• A syntactic approach to foundational proof-carrying code
• Coalgebraic semantics and observational equivalences of an imperative class-based OO-language
• Comparing object encodings.
• Considerate reasoning and the Composite design pattern
• Deep specifications and certified abstraction layers
• Fickle: Dynamic Object Re-classification
• GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept
• Hoare logic and auxiliary variables
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Local reasoning for global invariants. II: Dynamic boundaries
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14--18, 2005. Proceedings.
• Mathematics of Program Construction
• Modular invariants for layered object structures
• Positive subtyping
• Program logics for certified compilers
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• Separation logic and abstraction
• Separation logic, abstraction and inheritance
• Types and programing languages
• Verified software units

Cited in

(5)

• Verified software units
• Abstraction and subsumption in modular verification of C programs
• Sound modular verification of C code executing in an unverified context
• Efficient extensional binary tries
• Abstraction and subsumption in modular verification of C programs

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Verified software units

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233451)