Important Dates
- Registration by the 1st of December.
- Meeting on the 7th and 8th of December 2010.
Topic
Classically, model-checking techniques were developed for finite-state systems and applied to the verification of hardware and the control flow of programs. A fundamental challenge in software model-checking is to deal with rich data, residing in variables or on the heap. Variables may take their values from infinite domains (e.g. integers, strings, or even functions in higher-order programs) but only a limited number of operations on them are allowed. Data structures stored on the heap can be manipulated in almost arbitrary ways, but are often enforced to appear only in specific shapes (e.g. list, heaps, or trees). The classical methods can be extended to handle rich data by the use of abstraction, but this approach if often too coarse and does not fully exploit the restrictions on shape and operations on variables. We will discuss models which directly work with the exact data domain and structures and thus allow for more exact model-checking.
In the recent years there was a notable effort in extending classical methods of automata theory, computational logic and rewriting to richer models. Automata on words and trees augmented with data coming from an infinite alphabet (such as register automata working on data words) show how comparison of variables with values in an infinite domain can be handled in the framework of automata theory. On the other hand, rich classes of infinite structures have been found, for which key problems (model-checking, reachability, coverability) are decidable. Recursion schemes, vector addition systems, and graphs of bounded clique-width are examples of such structures enjoying nice decidable properties. These new techniques can be used to faithfully represent complete states of programs (including variable values and data structures on the heap) and allow to verify properties directly on such representation.
The aim of this workshop is to bring together researchers from both practical and theoretical sides, and to investigate how the recently developed tools in automata theory and logic can be used to model and verify programs with both rich data structures and data values.
Sponsors
The meeting is sponsored by the AutoMathA Project of the European Science Foundation.