Filip Konečný, Jiří Šimáček, Zdeněk Letko a Ondřej Lengál
FIT A113 - 13:00 31.3.2011
Filip Konečný: Interprocedural Reachability Analysis of Integer Programs
We will build on the previous presentation which described
techniques for reachability analysis of counter automata (CA)
a.k.a. non-deterministic integer programs. In effect, these
techniques compute the reachability relation of a CA (procedure
summary) -- a relation between values of counters at the beginning
and at the end of runs of CA. In this presentation, we will
explain how these summaries are used in reachability analysis of
hierarchical counter automata a.k.a. procedural non-deterministic
integer programs. We will also discuss the ongoing work --
reachability analysis of recursive integer programs.
Jiří Šimáček: Verification of programs with pointers using tree automata
We develop a verification method based on a novel use of tree automata
to represent heap configurations. A heap is split into several
"separated" parts such that each of them can be represented by a tree
automaton. Such heap representation is then used for checking safety
properties of sequential C programs manipulating dynamically linked data
Zdeněk Letko: New Concurrency Coverage Metrics
Current state of the art in concurrency coverage metrics will be presented and disadvantages of these metrics highlighted. Then, several new metrics designed with emphasis on capturing only interesting (in terms of concurrency errors detection) behavior of the program under test will be introduced. And finally, connection of this work with the topic of my dissertation will be mentioned.
Ondřej Lengál: Efficient Algorithms for Using Automata in Infinite-State Verification
The structure of many computer systems resembles trees which may often be conveniently represented using finite tree automata. This fact can be exploited for infinite-state verification of such systems. This presentation introduces our new approach for BDD-based symbolic representation of finite tree automata with large alphabets and discusses design of algorithms for automata operations over this structure.