Abstract: Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead the concrete domain. Familiar data-flow analysis algorithms are examples of abstract interpretation. In particular, abstract interpretation can be used for building the abstract state-space of the system. Many abstraction techniques have been proposed in the literature, and many of them deal with data type reduction, that is the reduction of a large (possible unbounded) data type to a small one. Prominent examples include shape analysis, predicate abstraction, the technique of duplicating predicate symbols, etc. In this presentation we try to capture the essence of data type reduction. In order to do that we consider data types modeled as universal algebras and define abstractions by means of congruences. The properties we want to prove are formulas in a 3-valued first order logic associated to the data type. We distinguish between three types of abstractions, ∀∀, ∃∀ and ∀∃, and for each of them we provide preservation results. Thus, we show that the ∀∀-abstractions are strong preserving, the ∃∀-abstractions are error preserving, and the ∀∃-abstractions are weak preserving. The generality of our approach is proved by showing that McMillan's approach, shape analysis, predicate abstraction, and the technique of duplicating predicate symbols can be viewed as particular cases of this approach. Finally, we take into consideration equationally specified data types. The abstraction is applied here to the initial algebra of such specifications by means of equations. Consistent examples, such as the keeping-up program and the bakery algorithm, are discussed.

Biography: Ferucio Laurentiu Tiplea is Professor at the Faculty of Computer Science, "Al.I.Cuza" University of Iasi, Romania. His research interests lie in the area of theories and tools for high-level modeling, design, and analysis of systems (including Petri nets and formal verification), formal languages and automata, computability and complexity, variable length codes and applications, cryptography and computer security, and algebraic foundations of computer science. The newest line of research is in using model checking to analyze finite abstractions of systems, with a specific focus on distributed system protocols such as those found in the security and electronic commerce domains. Dr. Tiplea published more than 50 papers in professional journals and refereed conference proceedings in these areas, co-authored two books on Petri net theory, and authored one book on set theory.