Automatic abstraction for intervals using Boolean formulae

DOI10.1007/978-3-642-15769-1_11MaRDI QIDQ4930724zbMATH OpenOpenAlexFDO

Authors Jörg Brauer, Andy King

Publication date 1 October 2010

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://kar.kent.ac.uk/30633/1/main.pdf

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Transfer function synthesis without quantifier elimination
• Automatic abstraction for bit-vectors using decision procedures
• Transfer function synthesis without quantifier elimination
• Automatic modular abstractions for template numerical constraints
• Automatic modular abstractions for linear constraints

Cited in

(8)

• Abstract interpretation of microcontroller code: intervals meet congruences
• Range and set abstraction using SAT
• Sound bit-precise numerical domains
• Automatic repair of overflowing expressions with abstract interpretation
• Automatic abstraction for bit-vectors using decision procedures
• Transfer function synthesis without quantifier elimination
• Transfer function synthesis without quantifier elimination
• Cost analysis of object-oriented bytecode programs

Describes a project that uses

Uses Software

• Sat4j
• Octagon

This page was built for publication: Automatic abstraction for intervals using Boolean formulae

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