Program invariants as fixedpoints

DOI10.1007/BF02248730zbMath0399.68022OpenAlexW138086306MaRDI QIDQ1254848

Edmund M. Clarke

Publication date: 1979

Published in: Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf02248730

zbMATH Keywords

Fixedpoint TheoremsFloyd-Hoare Axiom SystemsPredicate TransformersProgram Invariants

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (9)

Differential Game Logic ⋮ Stratified least fixpoint logic ⋮ Unnamed Item ⋮ The Birth of Model Checking ⋮ Computing Differential Invariants of Hybrid Systems as Fixedpoints ⋮ SMT-based model checking for recursive programs ⋮ Meanings of Model Checking ⋮ Semantics of algorithmic languages ⋮ Computing differential invariants of hybrid systems as fixed points

Cites Work

• Consistent and complementary formal theories of the semantics of programming languages
• Grammar Analysis and Parsing by Abstract Interpretation
• A Complete and Consistent Hoare Axiomatics for a Simple Programming Language
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• An axiomatic basis for computer programming
• Formalization of Properties of Functional Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Program invariants as fixedpoints