Transfer Function Synthesis without Quantifier Elimination

DOI10.1007/978-3-642-19718-5_6zbMath1326.68080arXiv1207.4286OpenAlexW1483082920MaRDI QIDQ5892491

Andy King, Jörg Brauer

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

Mathematics Subject Classification ID

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

Related Items (2)

Abstract interpretation of microcontroller code: intervals meet congruences ⋮ Fully Bounded Polyhedral Analysis of Integers with Wrapping

Uses Software

• Sat4j
• CBMC
• Mjollnir

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