vmcai13.pdf (248.81 kB)
Logico-numerical max-strategy iteration
chapter
posted on 2023-06-09, 01:05 authored by Peter Schrammel, Pavle SuboticStrategy 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.
History
Publication status
- Published
ISSN
0302-9743Publisher
SpringerExternal DOI
Volume
7737Page range
414-433Book title
Verification, Model Checking, and Abstract InterpretationISBN
9783642358739Series
Lecture Notes in Computer ScienceDepartment affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2016-05-09Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC