Skip to Main content Skip to Navigation
Conference papers

Logico-Numerical Max-Strategy Iteration

Peter Schrammel 1, * Pavle Subotic 2
* Corresponding author
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Strategy iteration methods are used for solving fixed point equations. It has been shown that they improve precision in static analysis based on abstract interpretation and template abstract domains, e.g. intervals, octagons or template polyhedra. However, they are limited to numerical programs. In this paper, we propose a method for applying max-strategy iteration to logico-numerical programs, i.e. programs with numerical and Boolean variables, without explicitly enumerating the Boolean state space. The method is optimal in the sense that it computes the least fixed point w.r.t. the abstract domain; in particular, it does not resort to widening. Moreover, we give experimental evidence about the efficiency and precision of the approach.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-00756833
Contributor : Peter Schrammel <>
Submitted on : Friday, November 23, 2012 - 6:28:45 PM
Last modification on : Tuesday, February 9, 2021 - 3:24:16 PM
Long-term archiving on: : Sunday, February 24, 2013 - 3:55:32 AM

Files

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00756833, version 1

Collections

CNRS | INRIA | LIG | UGA

Citation

Peter Schrammel, Pavle Subotic. Logico-Numerical Max-Strategy Iteration. Verification, Model Checking, and Abstract Interpretation, Jan 2013, Rome, Italy. pp.414-433. ⟨hal-00756833⟩

Share

Metrics

Record views

675

Files downloads

839