Invited Talk Abstracts
Unifying Invited Talk: Model Checking for Nominal Calculi
Model checking has been shown very effective for proving properties of system behavior whenever a finite model of it can be constructed. The approach is convenient since it does not require formal proofs and since the same syntax-free automaton-like model can accommodate system specification languages with substantially different syntax and semantics. Among the properties which can be checked, behavioral equivalence is especially important for matching specifications and implementations, for proving the system resistant to certain attacks and for replacing the system with a simpler one with the same properties. Names have been used in process calculi for representing a variety of different informations concerning addresses, mobility links, continuations, localities, causal dependencies, security keys and session identifiers. When an unbound number of new names can be generated during execution, the models tend to be infinite even in the simplest cases, unless explicit mechanisms are introduced to allocate and garbage collect names, allowing the same states to be reused with different name meanings. The talk reviews some existing syntax-free models for name-passing processes and focuses on History-Dependent (HD) automata, introduced by Montanari and Pistore in 1995. Process calculi exhibiting causality, localities and mobility, and Petri nets, can be translated - preserving bisimilarity - to HD automata. Different versions of HD automata have been defined. The simplest version can be easily translated to ordinary automata - but possibly with a much larger number of states - when handling causality, locality and the kind of mobility exhibited by the synchronous pi-calculus without matching. The front end towards the pi-calculus and the translation algorithm have been implemented in the HAL tool, which relies on the JACK verification environment for handling the resulting ordinary automata. In a second version, the states are equipped with name symmetries which further reduce the size of the automata. Furthermore, a theory based on coalgebras in a category of "named sets" can be developed for this kind of automata, which extends the applicability of the approach to all the kinds of pi-calculi and which guarantees the existence of the minimal automaton within the same bisimilarity class. The minimization algorithm, naturally suggested by the coalgebraic framework, has been implemented in the MIHDA toolkit within the European project PROFUNDIS. Other versions of HD automata can be equipped with algebraic operations, thus relying on an algebraic-coalgebraic, namely bialgebraic, theory. Here we propose a further instance handling the symbolic version of nominal calculi, where inputs are represented as variables which are instantiated only when needed. As it is the case for logic programming unification, one would like the variables to be instantiated only the least possible, still guaranteeing that all behaviors are eventually explored. The approach we follow relies on the notion of reactive system,introduced by Leifer and Milner and further developed in the PhD thesis by Pawel Sobocinski using G-categories and adhesive categories. The reduction semantics of reactive systems is extended in order to introduce as borrowed contexts both the variable instantiations needed in the transitions and the ordinary pi-calculus actions. Finally it is argued that the symbolic semantics model based on borrowed contexts can be conveniently applied to web service composition. (Joint work with Gianluigi Ferrari and Emilio Tuosto)
Unifying Invited Talk: Esterel v7: From Verified Formal Specification to Efficient Industrial Designs
Synchronous languages were developed in the mid-80's specifically to deal with embedded systems. They are based on mathematical semantics and support formal compilation to classical software or hardware languages as well as formal verification. Esterel v7 is a major industrial evolution of the original Esterel synchronous language, mostly directed to complex hardware appplications. The language is supported by the Esterel Studio integrated development environment, which provides a smooth path from verifiable executable specification to efficient circuit synthesis. The graphical Safe States Machines derived from Esterel are also used in the SCADE tool which is widely used for safety-critical software applications in avionics.
Through the examples of Esterel v7 and SCADE, we discuss the impact and evolution of formal methods for actual industrial design. In particular, we discuss some issues that are central for actual applications but are usually either not considered as such or viewed as too difficult to handle in research or R&D projects. We demonstrate that the difference between industrial success and failure often lies in precisely these aspects.
FOSSACS Invited Talk: Mathematical Models of Computational and Combinatorial Structures
The general aim of this talk is to advocate a combinatorial perspective, together with its methods, in the investigation and study of models of computation structures. This, of course, should be taken in conjunction with the well-established views and methods stemming from algebra, category theory, domain theory, logic, type theory, etc. In support of this proposal I will show how such an approach leads to interesting connections between various areas of computer science and mathematics; concentrating on one such example in some detail. Specifically, I will consider the line of my research involving denotational models of the pi-calculus and algebraic models of abstract syntax with variable binding, indicating how the abstract mathematical structure underlying these models fits with that of Joyal's combinatorial species of structures. This analysis suggests both the unification and generalisation of models, and in the latter vein I will introduce generalised species of structures. These generalised species encompass and generalise the various notions of species used in combinatorics. Furthermore, they have a very rich mathematical structure (akin to models of Girard's linear logic) that can be described purely within Lawvere's generalised logic. Indeed, I will present and treat the cartesian closed structure, the linear structure, the differential structure, etc. of generalised species axiomatically in this mathematical framework. As an upshot, I will observe that the setting allows for interpretations of computational calculi (like the lambda calculus, both typed and untyped; the recently introduced differential lambda calculus of Ehrhard and Regnier; etc.) that can be directly seen as translations into a more basic elementary calculus of interacting agents that compute by communicating and operating upon structured data.
Marcelo P. Fiore
FASE Invited Talk: Checking Memory Safety with Blast
Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how Blast can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use Ccured, a type-based memory safety analyzer, to annotate all program points that could not be proved to be memory safe within the type system with run time checks. Second, we use Blast to remove as many of these run time checks as possible (by proving that the checks never fail) and to generate counterexample traces for all run time checks that may fail. Our experience shows that Blast can remove many run time checks added by Ccured, and for the rest, point out error paths in the program that may cause a run time check to fail. Thus the combination of Ccured and Blast guarantees memory-safe programs without additional runtime overheads.
ESOP Invited Talk: Programming with Explicit Security Policies
Are computing systems trustworthy? To answer this, we need to know three things: what the systems are supposed to do, what they are not supposed to do, and what they actually do. All three are problematic. There is no expressive, practical way to specify what systems must do and must not do. And if we had a specification, it would likely be infeasible to show that existing computing systems satisfy it. If we can't analyze security after the fact, the alternative is to design it in from the beginning: accompany programs with explicit, machine-checked security policies, written by programmers as part of program development.
Trustworthy systems must safeguard the end-to-end confidentiality, integrity, and availability of information they manipulate. We currently lack both sufficiently expressive specifications for these information security properties, and sufficiently accurate methods for checking them. This talk describes progress on both fronts. First, information security policies can be made more expressive than simple noninterference or access control policies, by adding notions of ownership, declassification, robustness, and erasure. Second, program analysis and transformation can be used to provide strong, automated security assurance. The talk describes the application of these methods to building a distributed system with explicit security policies.
CC Invited Talk: When Abstraction Fails
Reasoning about programs is mostly deduction: the reasoning from the abstract model to the concrete run. Deduction is useful because it allows us to predict properties of future runs - up to the point that a program will never fail its specification. However, even such a 100% correct program may still show a problem: the specification itself may be problematic, or deduction required us to abstract away some relevant property.
To handle such problems, deduction is not the right answer - especially in a world where programs reach a complexity that makes them indistinguishable from natural phenomena. Instead, we should enrich our portfolio by methods proven in natural sciences, such as observation, induction, and in particular experimentation. In my talk, I will show how systematic experimentation automatically reveals the causes of program failures - in the input, in the program state, or in the program code.
TACAS Invited Talk: Applications of Craig Interpolation in Model Checking
A Craig interpolant for a mutually inconsistent pair of formulas (A,B) is a formula that is (1) implied by A, (2) inconsistent with B, and (3) expressed over the common variables of A and B. It is known that a Craig interpolant can be efficiently derived from a refutation of A & B, for certain theories and proof systems. For example, interpolants can be derived from resolution proofs in propositional logic, and for systems of linear inequalities over the reals. These methods have been recently extended to combine linear inequalities with uninterpreted function symbols, and to deal with integer models. One key aspect of these procedures is that they yield quantifier-free interpolants when the premises A and B are quantifier-free.
This talk will survey some recent applications of Craig interpolants in model checking. We will see that, in various contexts, interpolation can be used as a substitute for image computation, which involves quantifier elimination and is thus computationally expensive. The idea is to replace the image with a weaker approximation that is still strong enough to prove some property.
For example, interpolation can be used to construct an inductive invariant for a transition system that is strong enough to prove a given property. In effect, it gives us an abstract image operator that can be iterated to a fixed point to obtain an invariant. This invariant contains only information actually deduced by a prover in refuting counterexamples to the property of a fixed number of steps. Thus, in a certain sense, we abstract the invariant relative to a given property. This avoids the complexity of computing the strongest inductive invariant (i.e., the reachable states) as is typically done in model checking.
This approach gives us a complete procedure for model checking temporal properties of finite-state systems that allows us to exploit recent advances in SAT solvers for the proof generation phase. Experimentally, this method is found to be quite robust for verifying properties of industrial hardware designs, relative to other model checking approaches. The same approach can be applied to infinite-state systems, such as programs and parameterized protocols (although there is no completeness guarantee in this case). For example, it is possible to verify systems of timed automata in this way, or simple infinite-state protocols, such as the N-process "bakery" mutual exclusion protocol.
Alternatively, interpolants derived from proofs can be mined to obtain predicates that are useful for predicate abstraction,as is done in the Blast software model checker. This approach has been used in a software model checking to verify properties of C programs with in excess of 100K lines of code. Finally, interpolation can be used to approximate the transition relation of a system relative to a given property. This is useful in predicate abstraction, where constructing the exact abstract transition relation is prohibitive.