Verification Seminar

We introduce streaming string transducers that map input strings to output strings in a single left-to-right pass. The transducer uses a finite set of states, and a finite set of variables ranging over strings. At every step, it can make decisions based on the next input symbol, updating its state, and updating string variables by concatenating string variables and new symbols from the output alphabet. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over input/output strings, are in PSPACE. There is a robust and well-studied class of ``regular'' transductions on finite alphabets. This class of transductions can be defined by two-way deterministic finite-state transducers and it has a logical MSO-based characterization. We establish that the streaming string transducers capture exactly the class of regular transductions.
For applications to program verification, we define data streaming string transducers (DSSTs) that operate on data strings. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data domain that supports only the operations of equality and ordering. We identify a class of imperative and a class of functional programs, manipulating lists of data items, which can be effectively translated to DSSTs. The imperative programs dynamically modify a singly-linked heap by changing next-pointers of heap-nodes and by adding new nodes. The main restriction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.
This is joint work with Rajeev Alur.

Even with impressive advances in automated formal methods, certain problems in system verification and synthesis remain challenging. Examples include the verification of quantitative properties of software involving constraints on timing and energy consumption, and the automatic synthesis of systems from specifications. The challenges mainly arise from three sources: environment modeling, incompleteness in specifications, and the complexity of underlying decision problems. In this talk, I will present SCIDUCTION, a methodology to tackle these challenges. Sciduction combines inductive inference (learning from examples), deductive reasoning (such as SAT/SMT solving), and structure hypotheses. We have demonstrated several applications of sciduction including timing analysis of embedded software, synthesis of loop-free programs, synthesis from temporal logic (LTL), term-level verification of hardware (RTL) designs, and switching logic synthesis of hybrid systems. This talk will present some core theory, a couple of illustrative applications, and directions for future work.

The verification of programs that use pointers to implement dynamic data structures is a highly challenging and important task, as e.g. memory leaks or dereferencing null pointers can cause great damage especially when software reliability is at stake. But with object creation at runtime, dynamic data structures induce a possibly infinite state space and therefore cannot be handled by standard verification algorithms.
A common approach to solve this problem is to apply abstraction techniques. In this talk I will present you an abstraction technique based on hyperedge replacement grammars, which can be used to partially abstract and concretise heap structures. We will investigate some requirements that have to be met in order to guarantee a correct abstraction technique. Furthermore I will give you a short introduction to our verification tool "Juggrnaut" as well as some experimental results.