Transfer Function Synthesis without Quantifier Elimination
From MaRDI portal
Publication:5892491
DOI10.1007/978-3-642-19718-5_6zbMath1326.68080arXiv1207.4286OpenAlexW1483082920MaRDI QIDQ5892491
Publication date: 19 May 2011
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1207.4286
Related Items (2)
Abstract interpretation of microcontroller code: intervals meet congruences ⋮ Fully Bounded Polyhedral Analysis of Integers with Wrapping
Uses Software
Cites Work
- Unnamed Item
- The two variable per inequality abstract domain
- Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
- The octagon abstract domain
- A structure-preserving clause form translation
- Affine relationships among variables of a program
- Monotone data flow analysis frameworks
- Safe bounds in linear and mixed-integer linear programming
- Optimal domains for disjunctive abstract interpretation
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Range and Set Abstraction using SAT
- Ranking Function Synthesis for Bit-Vector Relations
- Taming the Wrapping of Integer Arithmetic
- Automatic Abstraction for Congruences
- Static analysis of arithmetical congruences
- Automatic Abstraction for Intervals Using Boolean Formulae
- Automatic modular abstractions for linear constraints
- Tools and Algorithms for the Construction and Analysis of Systems
- Programming Languages and Systems
- Logic programming with satisfiability
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Transfer Function Synthesis without Quantifier Elimination
