Range and set abstraction using SAT

DOI10.1016/J.ENTCS.2010.09.003MaRDI QIDQ2814098zbMATH OpenOpenAlexWikidataFDO

Authors Edd Barrett, Andy King

Publication date 17 June 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2010.09.003

zbMATH Keywords

abstract domainsnumeric domainsrangessatisfiability solving

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Deciding Bit-Vector Arithmetic with Abstraction
• Automatic abstraction for bit-vectors using decision procedures
• Computer Aided Verification
• scientific article; zbMATH DE number 1982200
• Automatic abstraction for intervals using Boolean formulae

Cites work

• A scalable segmented decision tree abstract domain
• A structure-preserving clause form translation
• Affine relationships among variables of a program
• An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries
• Automatic abstraction for intervals using Boolean formulae
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Recovery of jump table case statements from binary code
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving the incremental satisfiability problem
• The octagon abstract domain
• Two variables per linear inequality as an abstract domain
• Verification, Model Checking, and Abstract Interpretation
• Why does Astrée scale up?

Cited in

(5)

• Set abstraction - an extension of all solutions predicate in logic programming language
• Abstract interpretation of microcontroller code: intervals meet congruences
• scientific article; zbMATH DE number 1004882 (Why is no real title available?)
• Computer Aided Verification
• Transfer function synthesis without quantifier elimination

Describes a project that uses

Uses Software

• SATIRE

This page was built for publication: Range and set abstraction using SAT

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