Deciding program properties via complete abstractions on bounded domains

DOI10.1007/978-3-031-22308-2_9zbMath1524.68077MaRDI QIDQ6164426

Nicolas Manini, Roberto Bruni, Roberta Gori

Publication date: 28 July 2023

Published in: Static Analysis (Search for Journal in Brave)

zbMATH Keywords

program transformationterminationbounded domainsabstract interpretationprogram equivalencecomplete abstraction

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A survey of verification techniques for parallel programs
• Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
• Analyzing Program Analyses
• Systematic design of program transformation frameworks by abstract interpretation
• Making abstract interpretations complete
• On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
• Classes of Recursively Enumerable Sets and Their Decision Problems

This page was built for publication: Deciding program properties via complete abstractions on bounded domains