Hiding information in completeness holes
Roberto Giacobazzi, University of Verona, Italy

Complete abstractions model precisely the complete understanding of program semantics by an approximate observer, modeled by an abstract interpreter. This corresponds to the possibility of replacing, with no loss of precision, concrete computations with abstract ones. The lack of completeness of the observer is therefore the corresponding of its poor understanding of program semantics, and provides the key aspect for designing a new family of methods and tools for well-defined and possibly provable secure practical code steganography and more in general code obfuscation. In this paper we will address these aspects by showing how abstract interpretation and in particular abstract domain transformations may play a key role in future design methods for code steganography and obfuscation.

[Presenter's Biography]
Tools for CSP
Markus Roggenbach, Swansea University, UK

Among the various frameworks for the description and modelling of reactive systems, process algebra plays a prominent role. It has proved to be suitable, e.g., at the level of requirement specification, at the level of design specification, and also for the formal analysis of systems. In this context, the process algebra CSP provides a well-established, theoretically thoroughly studied, and in industry applied formalism for the modelling and verification of concurrent systems. Its applications range from train control systems over software for the international space station to the verification of security protocols. In 2005, the CSP community celebrated its birthday with the workshop "Communicating Sequential Processes, the first 25 years".

From its beginning on, CSP came along with simulation techniques. Hoare's book "Communicating Sequential Processes" from 1985 devotes separate sections on how to implement a simulation of the CSP semantics in a functional programming language. For example, the tool ProBe is one of many simulators available. Concerning proofs, CSP originally started as a new branch of mathematics where proofs are to be carried out with paper and pen. Soon enough, however, model checking was developed for CSP, offering a fully automated proof technique. This endeavour has been so successful that the CSP model checker FDR has been available as a commercial product for more than 20 years.

Over the last 10 years interactive theorem proving tools also have become available for CSP, complementing model checking techniques. The aim here is to ease the analysis of infinite state systems. In 1997, Dutertre and Schneider presented a CSP encoding based on the theorem prover PVS. Their tool is tailored to the analysis of security protocols. With such theorem proving support it is also possible to directly analyze entire classes of systems. One result is, for instance, the mechanized proof that a certain family of systolic arrays is deadlock-free, independent of the number of processes involved.

Yet another effect of encoding CSP into theorem provers is that formalizing CSP can help to reveal flaws in the semantic construction of the language itself. In 1997 Wolff and Tej published a corrected Failure-Divergence model for CSP, which arose from an implementation of CSP using the theorem prover Isabelle/HOL. While Wolff and Tej use a so-called shallow encoding, Isobe and Roggenbach presented in 2005 the tool CSP-Prover, which provides a deep encoding of CSP in Isabelle/HOL. This kind of encoding allows to reflect on the language CSP itself. In 2006 Isobe and Roggenbach proved within CSP-Prover the completeness of an axiom system for the CSP stable failures model. This proof also lead to the correction of algebraic laws. In the perception of the CSP community such results demonstrate that presentations of CSP models and CSP axiom schemes must necessarily be accompanied by mechanised theorem proving tools.

The talk will discuss various proof tools for CSP, show examples of how to analyze systems using these tools, and will also cover recent developments such as the the tool HORAE, which is based on constraint satisfaction techniques, and the CSP-CASL Prover.

[Presenter's Biography]

Roberto Giacobazzi, University of Verona, Italy

Roberto Giacobazzi was born in 1964 in Modena, Italy. He received the Laurea degree in Computer Science in 1988 at the University of Pisa, and in 1993 he received the Ph.D. in Computer Science at the same university, with a Ph.D. thesis on semantic aspects of logic program analysis, under the supervision of Prof. Giorgio Levi. From 1993 to 1995 he had a Post Doctoral Research position at Laboratoire d'Informatique (LIX), Ecole Polytechnique (Paris) in the equipe Cousot. From 1995 to 1998 he was Assistant Professor in Computer Science at the University of Pisa. From 1998 to 2000 he was Associate Professor at the University of Verona. From May 2000 until now he is Full Professor in computer science at the University of Verona. He is now Dean of the Faculty of Science of the University of Verona. The research interests of Roberto Giacobazzi include abstract interpretation, static program analysis, semantics of programming languages, program verification, abstract model-checking, program transformation and optimization, code obfuscation, software watermarking and lattice theory. He is author of more than 60 publications in international journals and conferences and he is involved in national (italian) and international (european) research projects in the field of static program analysis and code transformation. His main current research interest is in formal methods for systematic design of domains for abstract interpretation, with application in security, code obfuscation, semantics, program analysis, and abstract model-checking. In the past, he gave a declarative semantics for Prolog control features and he studied new methodologies to design static program analyzers and optimization techniques for logic and constraint-based languages by abstract interpretation. In lattice theory he studied the structure of the lattice of closure operators and complete congruence relations on complete lattices.

[Tutorial Abstract] [Keynote Presentation Abstract]
Markus Roggenbach, Swansea University, UK

Markus Roggenbach is a lecturer of Computer Science in the School of Physical Sciences at Swansea University, Wales, United Kingdom. He studied Mathematics and Computer Science in Braunschweig and Karlsruhe. He received his Ph.D. with a dissertation on "Abstract Characterizations of Bisimulation" from Mannheim University. As a post-doc in Bremen, he actively participated in the international Common Framework Initiatiative for algebraic specification and development of software. In 2003, he moved to Swansea, where he built up a research group on "Processes and Data". His research activities concern the modelling, verification, and validation of distributed systems. His interests span over semantics, logics, design of specification languages, interactive theorem proving, testing, formal methods and their industrial applications, with the main focus on algebraic specification and process algebra. In 2008, he became a member of the IFIP WG 1.3 Foundations of System Specification.

[Keynote Presentation Abstract]
Thomas Magedanz, Technische Universität Berlin, Germany

Thomas Magedanz (PhD) is full professor in the electrical engineering and computer sciences faculty at the Technische Universität Berlin, Germany, leading the chair for next generation networks ( In addition, he is director of the "next generation network infrastructure" division of the Fraunhofer Institute FOKUS (, which also provides various testbeds and tools in the context of Next Generation Networks and Open Converged Service Environments. The most popular ones include the Open Source IMS Core ( and the Open IMS Playground ( established in 2004. In 2007 he opened the new Open SOA Telco Playground ( for IMS/Web2.0/SOA service prototyping.

Since more than 20 years Prof. Magedanz is working in the convergence field of fixed and mobile telecommunications, the internet and information technologies, which resulted in many international R&D projects centered around Next Generation Service Delivery Platforms based on the afore mentioned testbeds.

[Tutorial Abstract]
Tiziana Margaria, Potsdam University, Germany

Tiziana Margaria is full professor at the University of Potsdam, where she holds the Chair of Service and Software Engineering.

She has broad experience in the use of formal methods for high assurance systems, in particular concerning functional verification, reliability, and compliance of complex heterogeneous systems, through major industrial projects. Her current focus is on formal methods supporting reliability and compliance through a model-driven version of service-oriented development. This concerns in particular the adequate treatment of third party components, as well as issues like policies, compliance, service-level agreement, fault tolerance, runtime monitoring, and system evolution. The industrial applications of the jABC framework, developed with her guidance, has proven the practicality of this holistic approach.

Prof. Margaria is President of the "European Association of Software Science and Technology" (EASST), member of the Board of FMICS (the ERCIM Working Group on Formal Methods for Industrial Critical Systems), serves as a member of the steering committee of ETAPS, the European joint Conferences on Theory and Practice of Software. She is editor of the Springer Book on the results of the Semantic Web Service Challenge. She is member of SAP’s PTLC (Platform Thought Leadership Council), that fosters a rapid and safe eSOA Adoption.

[Tutorial Abstract]
Created: Tue Feb 26 09:01:26 CST 2008
Last modified: Thu Jun 12 13:37:42 CST 2008
Maintained by Antonio Cerone