Sound bit-precise numerical domains

DOI10.1007/978-3-319-52234-0_27zbMATH Open1484.68053OpenAlexW2570093519MaRDI QIDQ2961585FDOQ2961585

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

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

Uses Software

• LLVM
• PPL
• Verasco

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)