Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

### lunes 4 de marzo de 2013

11:00am Meeting room 302 (Mountain View), level 3

**Anthony W. Lin***, Post-doctoral Researcher**, U. of Oxford*

### Reversal-bounded Acceleration of Counter Systems

#### Abstract:

Automatic analysis of integer-manipulating programs is a main problem
in program analysis. Such programs are a basic building block of more
complex imperative programs (e.g. with linked lists or strings) since
analysis of the latter can often be reduced to analysis of the former
(e.g. by some variants of counter abstractions). Since they are
already Turing-complete, the challenge is to devise approximation
techniques that give useful answers in many cases. Following a
standard automata-theoretic approach, we will consider Minsky’s
counter systems as an abstraction of integer-manipulating programs,
i.e., finite-state automata with integer counters whose values can be
incremented/decremented by and compared against integer constants. In order to
analyze such systems, we will consider reversal-bounded
acceleration, which is an underapproximation technique that covers
runs of a fixed number of reversals between non-incrementing/non-decrementing
modes of the counters. We will show that reversal-bounded analysis of counter
systems is efficiently reducible to satisfiability of quantifier-free Presburger
formulas (in fact, NP-complete) and so can be solved using highly-optimized SMT
solvers like Z3. We have implemented a prototype of the reduction and
shows the efficacies of the technique on a few interesting examples
(e.g. derived from Linux device drivers) which other techniques (e.g.
predicate abstractions and bounded-model checking) cannot deal with.
This is a joint work with Matthew Hague, which has appeared in CAV'11 and
CAV'12.