 |
|
|
|
| Comète-Parsifal Seminar (Abstracts 2005) |
|
Calendar
2012 2011 2010 2009 2008 2007 2006 2005 2004Abstracts
Jan 17, 2005, 2pm.
Title: Verification of Non-Regular Properties
Speaker: Martin Lange
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 context-sensitive 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 Itai-Rodeh Leader Election for Anonymous Rings
Speaker: Jun Pang
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 Itai-Rodeh algorithm, these two algorithms are finite-state. 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
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
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 (pi-calculus, 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
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 general-purpose language covering various platforms ranging from wide-area 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 pi-calculus, etc., can be encoded into LMNtal.
Yet another view of LMNtal is a constructor-free linear concurrent logic language in which data structures are encoded as process structures. Constructor-freeness means that LMNtal links are zero-assignment 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 pi-calculus 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
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
The Mobile Resource Guarantees (MRG) project is developing Proof-Carrying 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 high-level 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)
High-level 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 well-typed 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
(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 type-based 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 finite-state 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 type-based 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 non-trivial 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 typed-based techniques for behavioural reasoning.
Thu Mar 17, 2005. 2pm
Title: Different aspects of anonymity
Speaker: Kostas Chatzikokolakis
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 Action-labelled Quantitative Transition Systems
Abstract:
This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of bisimulation from non-quantitative systems to quantitative ones. We then prove that any single state-metric corresponds to a bisimulation and that the greatest state-metric 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 action-labelled 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 proof-carrying code and proof-carrying authentication, where it is successfully used to specify and verify formal guarantees about the run-time behavior of programs. These real-world 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 occurs-checks. Second I present a novel execution model based on selective memoization and third I will discuss term indexing techniques to sustain performance in large-scale examples. As experimental results will demonstrate, these optimizations taken together constitute a significant step toward exploring the full potential of logical frameworks in real-world 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 syntax-with-binding (that's higher-order rewriting as well as things like the pi-calculus) without assuming a higher-order framework. Extended Nominal Rewriting exploits these ideas further to give a system with two kinds of binding --- "lambda-like" (inspired by the lambda-calculus) and "pi-like" (inspired by pi-calculus restriction). The two kinds of binding live side-by-side 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 proof-carrying 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 type-based and Hoare-style verifiers.
A new verifier is created by providing an untrusted executable extension module, which can incorporate directly pre-existing non-foundational verifiers based on data-flow 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 proof-carrying code, typed assembly language, and data-flow 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 pi-calculus 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 end-user 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 pi-calculus slightly customized to take into account notions of resources and I shall discuss acquisitions, transfers, limitations, deallocations, garbage-collection and perhaps a bit of error-handling.
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 Church-Turing thesis.
The result that interaction machines are more expressive than Turing machines seems to fly in the face of accepted dogma. In particular, the Church-Turing 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 Bio
Dina 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 Pi-Calculus. It is designed to model protocols and prove their security properties by means of transition and event-based semantics. SPL is based on the Dolev-Yao 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: Free-Algebra Models for the Pi-Calculus
Abstract:
I shall show how to generate models for the pi-calculus 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 pi-calculus models, full abstraction for bisimulation congruence, a Moggi-style 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:00-16: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 hand-tailored labels of process calculi.
Sep 29, 2005
Speaker: Claudia Faggian
Title: L-nets, a game model of concurrent interaction.
Abstract:
We present L-nets as a game model allowing for concurrent interaction. L-nets have been developed in the context of Ludics (Girard 2001), which can be seen as a game model of sequential interaction, abstracting away from proof-theory. In this talk we focus on L-nets as parallel strategies.
Strategies capturing sequential interaction, such as Hyland-Ong innocent strategies or Girard's designs, are based on trees; during an interaction (play, or run) the order between the actions is totally specified. L-nets 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 proof-theoretical point of view, a tree strategy can be seen as an abstract sequent calculus derivations, while an L-net appears as an abstract (multiplicative-additive) proof-net. Moreover, as a tree strategy is a particular case of L-net, 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 Pierre-Louis 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 cut-free 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 meta-theory 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 higher-order 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 branching-time temporal logics are defined, followed by an introduction to symbolic model checking and partial-order 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 Curry-Howard correspondence to the sequent calculus for classical logic.
The symmetry of the cut-elimination 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 call-by-name and call-by-value evaluations.
We will discuss some implementation issues, using a term graph rewriting technique, and present a non-standard 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 meta-theory 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 programming-style 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, semi-automated proof of cut-elimination for Girard's Logic of Unicity (LU). (Joint work with Dale Miller)
Page maintainer: Carlos Olarte