Improving Strategies via SMT Solving

DOI10.1007/978-3-642-19718-5_13zbMath1326.68093arXiv1101.2812OpenAlexW3121218067MaRDI QIDQ3000582

Thomas Martin Gawlitza, David Monniaux

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/1101.2812

Mathematics Subject Classification ID

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

Related Items (2)

Template-Based Unbounded Time Verification of Affine Hybrid Automata ⋮ Validating numerical semidefinite programming solvers for polynomial invariants

Uses Software

• Yices
• Aspic
• ASTREE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The octagon abstract domain
• The polynomial-time hierarchy
• Complete sets and the polynomial-time hierarchy
• 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.
• Static Analysis by Abstract Interpretation: A Mathematical Programming Approach
• Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
• Grammar Analysis and Parsing by Abstract Interpretation
• Precise Relational Invariants Through Strategy Iteration
• Accelerated Data-Flow Analysis
• Combining Widening and Acceleration in Linear Relation Analysis
• Games through Nested Fixpoints
• Polynomial Precise Interval Analysis Revisited
• Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely
• A constructive fixed point theorem for min-max functions
• Automatic modular abstractions for linear constraints
• Static Analysis
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• On Nonterminating Stochastic Games
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Static Analysis by Policy Iteration on Relational Domains
• Precise Fixpoint Computation Through Strategy Iteration
• Classes of Recursively Enumerable Sets and Their Decision Problems
• Computer Aided Verification
• Perspectives of System Informatics

This page was built for publication: Improving Strategies via SMT Solving