Sound bit-precise numerical domains

DOI10.1007/978-3-319-52234-0_27MaRDI QIDQ2961585zbMATH OpenOpenAlexFDO

Authors Tushar Sharma, Thomas Reps

Publication date 21 February 2017

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-52234-0_27

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Numerical algorithms for computer arithmetic, etc. (65Y04)

Recommendations

• scientific article; zbMATH DE number 1738295
• Fast polyhedra abstract domain
• Automatic abstraction for bit-vectors using decision procedures
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis

Cites work

• scientific article; zbMATH DE number 3938547 (Why is no real title available?)
• scientific article; zbMATH DE number 3610766 (Why is no real title available?)
• scientific article; zbMATH DE number 1948392 (Why is no real title available?)
• Automatic abstraction for intervals using Boolean formulae
• Automatic modular abstractions for template numerical constraints
• Computer Aided Verification
• Donut domains: efficient non-convex domains for abstract interpretation
• Fully Bounded Polyhedral Analysis of Integers with Wrapping
• Program Analysis Using Weighted Pushdown Systems
• Static Analysis in Disjunctive Numerical Domains
• SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities
• Taming the Wrapping of Integer Arithmetic
• The octagon abstract domain
• Theory of Computer Addition and Overflows
• Transfer function synthesis without quantifier elimination
• Two-level semantics and abstract interpretation
• Verification, Model Checking, and Abstract Interpretation
• Weighted pushdown systems and their application to interprocedural dataflow analysis

Cited in

(2)

• Automatic abstraction for bit-vectors using decision procedures
• A new abstraction framework for affine transformers

Describes a project that uses

Uses Software

• Verasco
• PPL
• LLVM

This page was built for publication: Sound bit-precise numerical domains

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