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 structures.

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.