Range and Set Abstraction using SAT

DOI10.1016/j.entcs.2010.09.003zbMath1342.68067OpenAlexW2003412429WikidataQ113318353 ScholiaQ113318353MaRDI QIDQ2814098

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 domainssatisfiability solvingrangesnumeric domains

Mathematics Subject Classification ID

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

Related Items (2)

Abstract interpretation of microcontroller code: intervals meet congruences ⋮ Transfer Function Synthesis without Quantifier Elimination

Uses Software

• SATIRE

Cites Work

• Why does Astrée scale up?
• The octagon abstract domain
• A structure-preserving clause form translation
• Affine relationships among variables of a program
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Two Variables per Linear Inequality as an Abstract Domain
• Solving SAT and SAT Modulo Theories
• A Scalable Segmented Decision Tree Abstract Domain
• An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries
• Solving the incremental satisfiability problem
• Automatic Abstraction for Intervals Using Boolean Formulae
• Verification, Model Checking, and Abstract Interpretation
• Recovery of jump table case statements from binary code

This page was built for publication: Range and Set Abstraction using SAT