Improving strategies via SMT solving
From MaRDI portal
Publication:3000582
DOI10.1007/978-3-642-19718-5_13zbMATH Open1326.68093arXiv1101.2812OpenAlexW3121218067MaRDI QIDQ3000582FDOQ3000582
Authors: Thomas Martin Gawlitza, David Monniaux 
Publication date: 19 May 2011
Published in: Programming Languages and Systems (Search for Journal in Brave)
Abstract: We consider the problem of computing numerical invariants of programs by abstract interpretation. Our method eschews two traditional sources of imprecision: (i) the use of widening operators for enforcing convergence within a finite number of iterations (ii) the use of merge operations (often, convex hulls) at the merge points of the control flow graph. It instead computes the least inductive invariant expressible in the domain at a restricted set of program points, and analyzes the rest of the code en bloc. We emphasize that we compute this inductive invariant precisely. For that we extend the strategy improvement algorithm of [Gawlitza and Seidl, 2007]. If we applied their method directly, we would have to solve an exponentially sized system of abstract semantic equations, resulting in memory exhaustion. Instead, we keep the system implicit and discover strategy improvements using SAT modulo real linear arithmetic (SMT). For evaluating strategies we use linear programming. Our algorithm has low polynomial space complexity and performs for contrived examples in the worst case exponentially many strategy improvement steps; this is unsurprising, since we show that the associated abstract reachability problem is Pi-p-2-complete.
Full work available at URL: https://arxiv.org/abs/1101.2812
Recommendations
Cites Work
- Combining Widening and Acceleration in Linear Relation Analysis
- Title not available (Why is that?)
- The octagon abstract domain
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The polynomial-time hierarchy
- Grammar Analysis and Parsing by Abstract Interpretation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- A constructive fixed point theorem for min-max functions
- On Nonterminating Stochastic Games
- Static analysis by abstract interpretation: a mathematical programming approach
- Computer Aided Verification
- Static Analysis by Policy Iteration on Relational Domains
- Precise Fixpoint Computation Through Strategy Iteration
- Complete sets and the polynomial-time hierarchy
- Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
- Precise Relational Invariants Through Strategy Iteration
- Accelerated Data-Flow Analysis
- Computing relaxed abstract semantics w.r.t. quadratic zones precisely
- Static Analysis
- Verification, Model Checking, and Abstract Interpretation
- Classes of Recursively Enumerable Sets and Their Decision Problems
- Perspectives of System Informatics
- A Quantifier Elimination Algorithm for Linear Real Arithmetic
- Games through Nested Fixpoints
- Title not available (Why is that?)
- Automatic modular abstractions for linear constraints
- Polynomial Precise Interval Analysis Revisited
- Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs
- Computer aided verification. 18th international conference, CAV 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings.
Cited In (7)
- Logico-numerical max-strategy iteration
- Block-wise abstract interpretation by combining abstract domains with SMT
- Template-based unbounded time verification of affine hybrid automata
- Abstract interpretation meets convex optimization
- Invariant generation through strategy iteration in succinctly represented control flow graphs
- Validating numerical semidefinite programming solvers for polynomial invariants
- Precise Relational Invariants Through Strategy Iteration
Uses Software
This page was built for publication: Improving strategies via SMT solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000582)
