
Calendar2012 2011 2010 2009 2008 2007 2006 2005 2004AbstractsJan 17, 2005, 2pm. Title: Verification of NonRegular Properties Speaker: Martin Lange Abstract: Temporal logics that are used for formal verification of programs need to  admit fast model checking to make verification feasible  be reasonably expressive to enable the verification of interesting properties. Unfortunately, these two requirements rather oppose each other, and the success of logics like CTL and LTL shows that in most cases performance seems to be more important than expressivity. This tendency is also enforced by the fact that formulas of more expressive temporal logics become a lot harder to understand. In this talk we introduce Fixpoint Logic with Chop (FLC), a temporal logic that is able to express even some contextsensitive properties. We will show how model checking games can be used to understand the properties expressed by its formulas. We will also discuss how to cope with the additional complexity in model checking FLC. Jan 18, 2005, 3pm. Title: Simplifying ItaiRodeh Leader Election for Anonymous Rings Speaker: Jun Pang Abstract:
We present two probabilistic leader election algorithms for anonymous unidirectional rings with FIFO channels, based on an algorithm from Itai and Rodeh. In contrast to the ItaiRodeh algorithm, these two algorithms are finitestate. So they can be analyzed using explicit state space exploration; we used the probabilistic model checker PRISM to verify, for rings up to size five, that eventually a unique leader is elected with probability one. Furthermore, we give a manual correctness proof for each algorithm, for arbitrary ring size. (Joint work with Wan Fokkink.) In the beginning of this talk, I will also give a short and general introduction to model checking. Slides Jan 25, 2005, 3pm. Title: Probabilistic anonymity Speaker: Catuscia Palamidessi Abstract:
The concept of anonymity comes into play in a wide range of situations, varying from voting and anonymous donations to postings on bulletin boards and sending mails. A formal definition of this concept has been given in literature in terms of nondeterminism. In this paper, we investigate a notion of anonymity based on probability theory, and we show that it can be regarded as a generalization of the nondeterministic one. We then formulate this definition in terms of observables for processes in the probabilistic $\pi$calculus, and propose a method to verify automatically the anonymity property. We illustrate the method by using the example of the dining cryptographers. Slides Tue Feb 8, 2005, 3pm. Title: On the expressiveness of spatial logics Speaker: Etienne Lozes Abstract:
Spatial logics are logical formalisms that allow to describe space through the combination of multiplicative and additive onnectives. Their theoretical foundation is the bunched implications logic, that has then inspired the separation logic in the context of axiomatic semantics of imperative programs manipulating pointers, the static ambient logic in the context of data mining, and spatial logics for concurrency (picalculus, ambients) in the context of process specification. I will first introduce these logics and their contexts, and then study how they are related to traditional formalisms for these contexts (classical logic, modal logic) considering expressiveneness issues such has elimination of logical connectives as adjuncts or quantifiers, or the question of the intensionality of these logics. Thu Feb 24, 2005, 3pm. Title: LMNtal: a Language Model with Logical Links and Membranes Speaker: Kazunori Ueda, Dept. of Computer Science, Waseda University, Tokyo Abstract:
LMNtal (pronouned "elemental") is a simple language model based on graph rewriting that uses logical variables to represent links and membranes to represent hierarchies. The two major goals of LMNtal are (i) to unify various computational models based on multiset rewriting and (ii) to serve as the basis of a truly generalpurpose language covering various platforms ranging from widearea to embedded computation. Another contribution of the model is it greatly facilitates programming with dynamic data structures. LMNtal is an outcome of the attempt to unify two extensions of concurrent logic programming, namely concurrent constraint programming and Constraint Handling Rules, where our focus has been multiset rewriting rather than constraint handling. At the same time, LMNtal can be regarded as a hierarchical multiset rewriting language augmented with logical links, and many computational models including Petri Nets, Gamma, the picalculus, etc., can be encoded into LMNtal. Yet another view of LMNtal is a constructorfree linear concurrent logic language in which data structures are encoded as process structures. Constructorfreeness means that LMNtal links are zeroassignment variables, where the purpose of a variable is to connect two points using a private identity. Multisets are supported by the membrane construct that allows both nesting and mobility. Logical links can represent (among other things) communication channels, but the key differences from picalculus channels are that (i) a message sent through a link changes the identity of the link and (ii) links are always private. The LMNtal system, running on a Java platform, has been released and the talk will include animating demonstrations of the system in addition to language issues. Mar 1, 2005 Title: Projective Membrane Calculus Speaker: Sylvain Pradalier Abstract:
This calculus is a refinement of L.Cardelli's Membrane Calculus which is a hierarchical process calculus corresponding to biological membranes. We bring revisions which make the calculus closer to biological membranes and which gives a pleasant invariant property. The calculus becomes indeed stable under symetries corresponding to shifting one's point of view. The corresponding structural equivalence may be of interest in other hierarchical calculus. Mon Mar 7, 2005, 11am Title: Automatic Certification of Resource Consumption Speaker: Alberto Momigliano Abstract:
The Mobile Resource Guarantees (MRG) project is developing ProofCarrying Code technology to endow mobile code with certificates of bounded resource consumption. These certificates should be generated by a compiler which, in addition to translating highlevel programs into machine code, derives formal proofs based on programmer annotations and program analysis. As the basis for reasoning and certificate generation, we employ a program logic for a subset of the JVM, implemented in Isabelle/HOL a' la Nipkow. Although, this has some niceties, such as the soundness and (relative) completeness, which we have formally verified, it proved less suited for concrete program verification, as it required a good deal of user interaction. We here present a derived logic which is defined on top of the core logic and directly relates to our compile time analysis. It encodes at the JVM level the interpretation of the type system of Hofmann and Jost for heap space consumption. The complexity of the side conditions in the new logic is significantly lower than those in the base logic, making automatic verification feasible. In fact, a fairly naive tactic will solve all the examples we have considered so far. If time permits, we will demo the whole MRG ``flow'', culminating in certificate generation. Mar 8, 2005, 3pm Title: Correspondence Assertions for Process Synchronization in Concurrent Communications Speaker: Eduardo Bonelli (LIFIA, Facultad de Informatica, UNLP, Argentina) Abstract:
Highlevel specification of patterns of communications such as protocols can be modeled elegantly by means of session types. However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions. The resulting type discipline augments the types of long term channels with effects and thus yields types which may depend on messages read/written prior within the same session. We prove that evaluation preserves typability and that welltyped processes are safe. Also, we illustrate how the resulting theory allows us to address the shortcomings present in the pure theory of session types. This is joint work with Adriana Compagnoni and Elsa Gunter. Tue Mar 15, 2005. 3pm Title: Axiomatisations and Types for Probabilistic and Mobile Processes Speaker: Yuxin Deng Abstract: (The talk is based on the PhD thesis of Yuxin Deng) This thesis focuses on the theoretical foundations of reasoning about algorithms and protocols for modern distributed systems. Two important features of models for these systems are probability and typed mobility, which are studied separately in this thesis. We develop algebraic techniques for behavioural reasoning on probabilistic processes and typed mobile processes. We also provide a typebased technique for verifying the terminating behaviour of some mobile processes. We first study the algebraic theory of a process calculus which combines both nondeterministic and probabilistic behaviour in the style of Segala and Lynch's probabilistic automata. We consider various strong and weak behavioural equivalences, and we provide complete axiomatisations for finitestate processes, restricted to guarded recursion in case of the weak equivalences. Then we investigate the impact of capability types on the algebraic theory of the $\pi$calculus. Capability types are useful for controlling resource access. They allow one to distinguish between the capability to read from a channel, to write to a channel, and both to read and to write. They also give rise to a natural and powerful subtyping relation. We consider two variants of typed bisimilarity, both in their late and in their early version. For both of them, we give complete axiomatisations on the closed finite terms. For one of the two variants, we provide a complete axiomatisation for the open finite terms. Finally we develop a typebased technique for verifying the termination property of some mobile processes. We provide four type systems to guarantee this property. The type systems are obtained by successive refinements of the types of the simply typed $\pi$calculus. The termination proofs take advantage of techniques from term rewriting systems. These type systems can be used for reasoning about the terminating behaviour of some nontrivial examples: the encodings of primitive recursive functions, the protocol for encoding separate choice in terms of parallel composition, a symbol table implemented as a dynamic chain of cells. These results lay out the foundations for further study of more advanced models which may combine probability with typed mobility. They also highlight the robustness of the algebraic and typedbased techniques for behavioural reasoning. Thu Mar 17, 2005. 2pm Title: Different aspects of anonymity Speaker: Kostas Chatzikokolakis Abstract: Anonymity is a concept which appears in various networking systems when users demand guarantees that their identity (and not necessarily the information they send) will remain secret. This talk is essentially a survey of various anonymity results. In the first part we will give some examples of scenarios where anonymity comes into play, from simple ones like the dining cryptographers problem to more realistic ones like the Crowds system for anonymous web browsing. Then we will examine different approaches to define anonymity, using process calculi, epistemic logic and domain theory concepts, briefly discussing their relation when possible. Tue Mar 22 2005. 3pm Speaker: Yuxin Deng Title: Metrics for Actionlabelled Quantitative Transition Systems Abstract: This paper defines actionlabelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define statemetrics as a natural extension of bisimulation from nonquantitative systems to quantitative ones. We then prove that any single statemetric corresponds to a bisimulation and that the greatest statemetric corresponds to bisimilarity. Furthermore, we provide two extended examples which show that our results apply to both probabilistic and weighted automata as special cases of actionlabelled trantitative transition systems. Mon May 2. 3pm Speaker: Brigitte Pientka Title:Overcoming Performance Barriers: efficient proof search in logical frameworks Abstract: The logical framework Twelf provides an experimental platform to specify, implement and execute formal systems. One of its applications is in proofcarrying code and proofcarrying authentication, where it is successfully used to specify and verify formal guarantees about the runtime behavior of programs. These realworld applications have exposed some critical bottlenecks: execution of many logical specifications is severely hampered and some are not executable at all, thereby limiting its application in practice. In this talk, I will describe three optimizations which substantially improve the performance and extend the power of the existing system. First, I give an optimized unification algorithm for logical frameworks which allows us to eliminate unnecessary occurschecks. Second I present a novel execution model based on selective memoization and third I will discuss term indexing techniques to sustain performance in largescale examples. As experimental results will demonstrate, these optimizations taken together constitute a significant step toward exploring the full potential of logical frameworks in realworld applications. Fri May 13. 10:30am Speaker: Prakash Panangaden Title:Anonymous Leader Election with Quantum Resources Joint work with Ellie D'Hondt Abstract: In this talk I discuss paradigmatic tasks from classical distributed computing  leader election and distributed consensus  in the presence of quantum resources. The main contribution is a demonstration of the special computational power of the W state, and also of the GHZ state. First, totally correct leader election is possible in anonymous quantum networks, which is in contrast with the classical situation. Next, we prove that the specific entanglement provided by the W and GHZ states, and their generalisations, is the only kind that exactly solves leader election and distributed consensus respectively. At the heart of the proofs of these impossibity results lie symmetry arguments. The talk will not assume special knowledge of quantum mechanics or quantum information theory. May 23 2005. 2pm Speaker: Jamie Gabbay Title:Extended Nominal Rewriting: Abstraction vs. Locality" Abstract: Nominal Rewriting allows you to express rewriting on syntaxwithbinding (that's higherorder rewriting as well as things like the picalculus) without assuming a higherorder framework. Extended Nominal Rewriting exploits these ideas further to give a system with two kinds of binding  "lambdalike" (inspired by the lambdacalculus) and "pilike" (inspired by picalculus restriction). The two kinds of binding live sidebyside in the system and interact, but are different. So we compare and contrast two different and powerful notions of abstraction, independently of the computational systems which gave rise to them. Because we have a rewrite system, we can also pass back to the original systems, and others, by writing down the rewrite rules. May 24 2005. 2pm Speaker: Giuseppe Castagna Title: A gentle introduction to semantic subtyping. Abstract: Subtyping relations are usually defined either syntactically by a formal system or semantically by an interpretation of types into an untyped denotational model. In this talk we show step by step how to define a subtyping relation semantically in the presence of functional types and dynamic dispatch on types, without the complexity of denotational models, and how to derive a complete subtyping algorithm. The presentation is voluntarily kept informal and discursive and the technical details are reduced to a minimum since we rather insist on the motivations, the intuition, and the guidelines to apply the approach. May 26 2005. 10:30am Speaker: George Necula Title:The Open Verifier Framework for Building Foundational Verifiers Abstract: We present the Open Verifier architecture for verifying untrusted code using customized verifiers. This framework can be viewed as an instance of foundational proofcarrying code where an untrusted program can be checked using the verifier most natural for it instead of using a single generic type system. Our design of the Open Verifier places special emphasis on reducing the burden of expressing both typebased and Hoarestyle verifiers. A new verifier is created by providing an untrusted executable extension module, which can incorporate directly preexisting nonfoundational verifiers based on dataflow analysis or type checking. We show how multiple extensions can cooperate for verifying programs that use foreign functions. The extensions control virtually all aspects of the verification by carrying on a dialogue with the Open Verifier using a language designed both to correspond closely to common verification actions and to carry simple adequacy proofs for those actions. We describe our experience implementing proofcarrying code, typed assembly language, and dataflow or abstract interpretation based verifiers (including a JVML bytecode verifier) in this unified setting. Wed 1 June 2005. 10:30AM Speaker: David Teller Title: Many Ressources, one picalculus to Control Them All Abstract: Numerous distribution techniques allow the composition of systems with limited resources (e.g. memory, cpu power or services) into more powerful systems with more resources, all this being, if possible, transparent to the enduser of the resources. On the other hand, theories of mobility deal with concurrent and distributed systems, from the point of view of transfers of informations, authorizations or agents, i.e. resources. During this talk, I will present a picalculus slightly customized to take into account notions of resources and I shall discuss acquisitions, transfers, limitations, deallocations, garbagecollection and perhaps a bit of errorhandling. Mon 6 June 2005. 3pm Speaker: Dina Goldin Title: Interaction: Conjectures, Results, Myths Abstract: It is commonly recognized that today's computing applications, such as web services, intelligent agents, operating systems, and graphical user interfaces, cannot be modeled by Turing machines and algorithms, which view computation as a closed box transformation of inputs to outputs. According to the interactive view of computation, communication (input/output) happens during the computation, not before or after it. This approach, distinct from either the theory of computation or concurrency theory, represents a paradigm shift that changes our understanding of what computation is and how it is modeled, promising to bridge these two fields. It had been conjectured (Wegner 1997) that "interaction is more powerful than algorithms". We present one model of interactive computation, Persistent Turing Machines (PTMs). PTMs extend Turing machines with dynamic streams and persistence to capture sequential interaction, which is a limited form of concurrency. They allow us to prove Wegner's conjecture and to formulate the Sequential Interaction Thesis, going beyond the expressiveness of the ChurchTuring thesis. The result that interaction machines are more expressive than Turing machines seems to fly in the face of accepted dogma. In particular, the ChurchTuring thesis is commonly interpreted to imply that Turing machines model all computation. We conclude by discussing the historical reasons for this common, but incorrect, interpretation. Speaker BioDina Q. Goldin is a faculty member in Computer Science & Engineering at the University of Connecticut and an adjunct faculty member in Computer Science at Brown University. Dr. Goldin obtained her B.S. in Mathematics and Computer Science at Yale University, and her M.S. and Ph.D. in Computer Science at Brown University. Her current topics of research are models of interaction and data models and query languages.Mon 13 June 2005. 10:30AM Speaker: Andres Aristizabal Title: An Introduction to SPL Abstract: SPL is an economic secure process calculus close to an asynchronous PiCalculus. It is designed to model protocols and prove their security properties by means of transition and eventbased semantics. SPL is based on the DolevYao model, which states that cryptography is unbreakable and that the spy is an active intruder capable of intercept, modify, replay and suppress messages. The calculus is operationally defined in terms of configurations containing items of information (messages) which can only increase during evolution. This models the fact that, in an open network, an intruder can see and remember any message that was ever in transit. In this talk I will give an introduction to SPL. Also, I will briefly describe my current and future work on Using SPL for Modeling and Analyzing P2P Protocols. Tue 14 June 2005. 10:30AM Speaker: Ian Stark Title: FreeAlgebra Models for the PiCalculus Abstract: I shall show how to generate models for the picalculus as free algebras for an equational theory; where the theory has separate components for name creation, communication of names over channels, and nondeterminism. This provides a modular characterisation of picalculus models, full abstraction for bisimulation congruence, a Moggistyle computational monad, and the bonus of an accompanying modal logic. The only tricky part is that it all has to be done within the functor category Set^I, using some general results of Power and Plotkin about enriched Lawvere theories. http://www.ed.ac.uk/~stark/freamp.html Sep 12, 2005 14:0016:00 Speaker: Pawel Sobocinski Title: Towards a general theory of labels from reductions. Abstract: The semantics of computational formalisms such as the lambda calculus and many process calculi can be formalised using rewrite systems. The underlying rewrite rules are pairs (redex and reactum) of open terms (that is, they contain process variables, or "holes"). Such rewrite rules, instantiated by arbitrary parameters and inserted into arbitrary evaluation contexts, give rise to a reduction relation. Such a relation can then be used to obtain reasonable notions of process equivalence. Leifer and Milner have used a simple and elegant procedure which identifies when a context is necessary to trigger reduction in a given closed term, assuming a rewrite system based on a set a ground rewrite rules (i.e. the redex and reactum are closed terms). Such minimal contexts can then be used to give labels to a labelled transition system on which bisimilarity is a congruence. Unfortunately, the restriction to ground rewrites means that if we are to study the lambda calculus or CCS directly in their framework, we must deal with infinitely many rules because all possible parameters have to be considered. We shall discuss a more refined approach which allows one to determine both the minimal context as well as the most general parameter necessary to trigger a reduction in a given open term. The analysis of our results raises interesting questions about the usually handtailored labels of process calculi. Sep 29, 2005 Speaker: Claudia Faggian Title: Lnets, a game model of concurrent interaction. Abstract: We present Lnets as a game model allowing for concurrent interaction. Lnets have been developed in the context of Ludics (Girard 2001), which can be seen as a game model of sequential interaction, abstracting away from prooftheory. In this talk we focus on Lnets as parallel strategies. Strategies capturing sequential interaction, such as HylandOng innocent strategies or Girard's designs, are based on trees; during an interaction (play, or run) the order between the actions is totally specified. Lnets on the contrary are based on graphs, and interactions are partial orders; the intuitionis that some actions can be performed in parallel (or scheduled in any order), while there are tasks which depend upon other tasks. When taking a prooftheoretical point of view, a tree strategy can be seen as an abstract sequent calculus derivations, while an Lnet appears as an abstract (multiplicativeadditive) proofnet. Moreover, as a tree strategy is a particular case of Lnet, we have a homogeneus setting, in which it is possible to move between different degrees of sequentiality. This talk is based on work in collaboration with Francois Maurel and with PierreLouis Curien. Oct 10,2005 Speaker: Lutz Strassburger Title: On the Role of Medial in a Boolean Category Abstract: In its most general meaning, a Boolean category is to categories what a Boolean algebra is to posets. In a more specific meaning a Boolean category should provide the abstract algebraic structure underlying the proofs in Boolean Logic, in the same sense as a Cartesian closed category captures the proofs in intuitionistic logic and a *autonomous category captures the proofs in linear logic. However, recent work has shown that there is no canonical axiomatisation of a Boolean category. In this work, we will see a series (with increasing strength) of possible such axiomatisations, all based on the notion of *autonomous category. We will particularly focus on the medial map, which has its origin in an inference rule in KS, a cutfree deductive system for Boolean logic in the calculus of structures. The talk is based on this paper. Oct 17, 2005 Speaker: Mohammad Reza Mousavi Title: SOS and all that ... Abstract: In the first part of this talk, I will present an overview of what has been going on in the last 20 years concerning the metatheory of SOS (Structured or Structural Operational Semantics). Then, I will focus more on our three recent contributions to this field regarding SOS with equational specifications, SOS with data and SOS for higherorder processes. The talk will be concluded by pointing out some ongoing research and future challenges. The material presented in this talk are the result of joint works with Michel A. Reniers, Jan Friso Groote and Murdoch J. Gabbay Oct 20, 2005 Speaker: Ugo Montanari Title: Hoare vs Milner: Comparing Synchronizations in a Graphical Framework with Mobility. Abstract: We compare the expressive power of Hoare (i.e., CSP style) and Milner (i.e., CCS style) synchronizations for defining graph transformations in a framework where edges can perform actions on adjacent nodes to synchronize their evolutions. Furthermore, nodes can be communicated and merged. We show that the expressive powers of the two synchronization models are different, but no one is greater than the other. Finally, we show that in many interesting cases the behaviour of a synchronization model can be mimicked by the other one using suitable translations for the rewritten graphs (joint work with Ivan Lanese). Nov 7, 2005 Speaker: Peng Wu Title: An Introduction to Model Checking ( Slides ) Abstract: We outline principles of model checking techniques for the automatic analysis of concurrent systems, then formally define a transition system(Kripke Model), temporal logics and their relationships. Basic model checking algorithms for linear and branchingtime temporal logics are defined, followed by an introduction to symbolic model checking and partialorder reduction techniques. Some more advanced topics will be discussed generally. Nov 8 and Nov 25 2005 Speaker: Peng Wu Title: An Introduction to Probabilistic Model Checking ( Slides ) Abstract: We introduce principles of probabilistic model checking techniques for the automatic analysis of (concurrent) probabilistic systems, then arrange various classes of probabilistic systems studied in the literatures in an expressiveness hierarchy. Probabilistic extensions of temporal logics are formally defined with corresponding model checking algorithms. Dec 5, 2005 Speaker: Steffen van Bakel Title: The language X: term rewriting, continuations and classical types Abstract: We will present the language X that describes a calculus of connecting that has been designed to give a CurryHoward correspondence to the sequent calculus for classical logic. The symmetry of the cutelimination procedure for proofs is reflected by a symmetry in the reduction relation on X. To demonstrate the expressive power of X, we will show how, even in an untyped setting, more and more elaborate calculi can be embedded into X. We describe how the symmetrical reductions of X account for the callbyname and callbyvalue evaluations. We will discuss some implementation issues, using a term graph rewriting technique, and present a nonstandard notion of decidable type assignment both on terms and graphs. Dec 12, 2005 Speaker: Elaine Pimentel Title: On the specification of sequent systems. Abstract: Recently, linear Logic has been used to specify sequent calculus proof systems in such a way that the proof search in linear logic can yield proof search in the specified logic. Furthermore, the metatheory of linear logic can be used to draw conclusions about the specified sequent calculus. For example, derivability of one proof system from another can be decided by a simple procedure that is implemented via bounded logic programmingstyle search. Also, simple and decidable conditions on the linear logic presentation of inference rules, called homogeneous and coherence, can be used to infer that the initial rules can be restricted to atoms and that cuts can be eliminated. In the present paper we introduce Llinda, a logical framework based on linear logic augmented with inference rules for definition (fixed points) and induction. In this way, the above properties can be proved entirely inside the framework. To further illustrate the power of Llinda, we extend the definition of coherence and provide a new, semiautomated proof of cutelimination for Girard's Logic of Unicity (LU). (Joint work with Dale Miller) Page maintainer: Carlos Olarte 