Verified software units
From MaRDI portal
Publication:2233451
DOI10.1007/978-3-030-72019-3_5zbMath1473.68035OpenAlexW3136796399MaRDI QIDQ2233451
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-72019-3_5
positive subtypingabstract predicate declarationresidual predicateverified software toolchainverified software unit
Theory of programming languages (68N15) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proof-carrying code from certified abstract interpretation and fixpoint compression
- A syntactic approach to foundational proof-carrying code
- Comparing object encodings.
- Positive subtyping
- Hoare logic and auxiliary variables
- Verified software units
- Modular invariants for layered object structures
- Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14--18, 2005. Proceedings.
- Fickle: Dynamic Object Re-classification
- Deep Specifications and Certified Abstraction Layers
- Separation logic, abstraction and inheritance
- Considerate Reasoning and the Composite Design Pattern
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Separation logic and abstraction
- Mathematics of Program Construction
- Local Reasoning for Global Invariants, Part II
- Program Logics for Certified Compilers
- GEDANKEN—a simple typeless language based on the principle of completeness and the reference concept
- Logic for Programming, Artificial Intelligence, and Reasoning
- Logic for Programming, Artificial Intelligence, and Reasoning
This page was built for publication: Verified software units
