Deciding program properties via complete abstractions on bounded domains

DOI10.1007/978-3-031-22308-2_9MaRDI QIDQ6164426zbMATH OpenFDO

Authors Roberto Bruni, Roberta Gori, Nicolas Manini

Publication date 28 July 2023

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-22308-2_9

zbMATH Keywords

abstract interpretationbounded domainscomplete abstractionprogram equivalenceprogram transformationtermination

Mathematics Subject Classification ID

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

Recommendations

• Making abstract interpretations complete
• Making abstract models complete
• Analyzing program analyses
• scientific article; zbMATH DE number 1759702

Cites work

• A survey of verification techniques for parallel programs
• Analyzing program analyses
• Classes of Recursively Enumerable Sets and Their Decision Problems
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• scientific article; zbMATH DE number 2161330 (Why is no real title available?)
• Making abstract interpretations complete
• On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
• Principles of abstract interpretation
• Sometime = always + recursion always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
• Systematic design of program transformation frameworks by abstract interpretation

Cited in

(3)

• Completeness of abstract domains for string analysis of JavaScript programs
• Optimal Abstraction on Real-Valued Programs
• On the Monniaux problem in abstract interpretation

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

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