Papers & Software





Comète-Parsifal Seminar (Abstracts 2010)


2012 2011 2010 2009 2008 2007 2006 2005 2004
Mon Nov 29, 10:30Rohit Chadha Model Checking Concurrent Programs with Nondeterminism and Randomization
Fri Nov 12, 16:45Filippo Bonchi Concurrency Cannot Be Observed, Asynchronously
Fri Oct 22, 10:30 Romain Demangeon Termination for concurrent processes
Fri Aug 27, 16:30Miguel Andres Information Hiding in Probabilistic Concurrent Systems
Fri Aug 27, 15:00Kohei Honda A Theory of Design-by-Contract for Distributed Multiparty Interactions
Fri Aug 27, 11:30Mario S. Alvim, Miguel Andres and Catuscia Palamidessi Information Hiding in Probabilistic Concurrent Systems
Fri Aug 27, 10:30Pierre-Malo Denielou Parameterised Multiparty Session Types
Thu Jul 01, 10:30 Carroll Morgan Noninterference, probability, Bayes Risk and compositionality
Fri May 28, 14:30Luis Fernando Pino Basic Concepts on Well Structured Transition Systems
Tue Apr 27, 10:00Jan Rutten, Filippo Bonchi and Ivan Gazeau (Linear) Weighted Automata, algorithms and an application for bounding errors
Mon Apr 26, 14:30 Alexandra Silva and Marcello Bonsangue Adding expressivity to Coalgebra Theory: all the equivalences of FT-coalgebras!!!
Mon Apr 26, 10:00Catuscia Palamidessi and Mario Alvim From Information Theory to Kantorovich Metric: an application to anonimity and leakage
Tue Mar 23, 10:30 Jeremy Avigad Decision procedures, heuristic procedures, and formally verified mathematics
Wed Mar 10, 15:00 Cienzia Di Giusto On the Computational Strenght of Higher Order and Passivation


Nov 29 2010, 10:30
Speaker: Rohit Chadha
Title: Model Checking Concurrent Programs with Nondeterminism and Randomization

For concurrent probabilistic programs/security protocols having process-level nondeterminism, it is often necessary to restrict the class of schedulers that resolve nondeterminism to obtain sound and precise model checking algorithms. We introduce two classes of schedulers called view consistent and locally Markovian schedulers and consider the model checking problem of concurrent, probabilistic programs under these alternate semantics. Specifically, given a Büchi automaton Spec, a threshold x in [0, 1], and a concurrent program P, the model checking problem asks if the measure of computations of P that satisfy Spec is at least x, under all view consistent (or locally Markovian) schedulers. We give precise complexity results for the model checking problem (for different classes of Buchi automata specifications) and contrast it with the complexity under the standard semantics that considers all schedulers. Joint work with A. Prasad Sistla and Mahesh Viswanathan.

Nov 12 2010, 16:45
Speaker: Filippo Bonchi
Title: Concurrency Can't Be Observed, Asynchronously

The paper is devoted to an analysis of the concurrent features of asynchronous systems. A preliminary step is represented by the introduction of a non-interleaving extension of barbed equivalence. This notion is then exploited in order to prove that concurrency cannot be ob- served through asynchronous interactions, i.e., that the interleaving and concurrent versions of a suitable asynchronous weak equivalence actually coincide. The theory is validated on two case studies, related to nominal calculi (π-calculus) and graphical specification formalisms (Petri nets).
Fri Oct 22 2010, 10:30
Speaker: Romain Demangeon
Title: Termination for concurrent processes

Ensuring termination is a challenging task in a concurrent setting where the topology of the systems can evolve dynamically (creation of new services, update of existing services, sharing of previously secret informations). We study the termination of the mobile processes in the formalism of the pi-calculi using static analysis such as type systems. We use methods coming both from the rewriting theory and the proof theory and present an original way of combining the two approaches, yielding increased expressiveness.
Aug 27 2010, 16:30
Speaker: Miguel Andres
Title: Information Hiding in Probabilistic Concurrent Systems

Information hiding is a general concept which refers to the goal of preventing an adversary to infer secret information from the observables. Anonymity and Information Flow are examples of this notion. We study the problem of information hiding in systems characterized by the presence of randomization and concurrency. It is well known that the raising of nondeterminism, due to the possible interleavings and interactions of the parallel components, can cause unintended information leaks. One way to solve this problem is to fix the strategy of the scheduler beforehand. In this work, we propose a milder restriction on the schedulers, and we define the notion of strong (probabilistic) information hiding under various notions of observables. Furthermore, we propose a method, based on the notion of automorphism, to verify that a system satisfies the property of strong information hiding, namely strong anonymity or no-intereference, depending on the context.
Aug 27 2010, 15:00
Speaker: Kohei Honda
Title: A Theory of Design-by-Contract for Distributed Multiparty Interactions

The approach known as Design by Contract (DbC) promotes reliable software development through elaboration of type signatures for sequential programs with logical formulae. In this talk I will present our recent work on an assertion method which generalises DbC baesd on multiparty session types. Centring on the notion of global assertions and their projections onto endpoints,the framework allows expressive specifications and validation while allowing effective static and dynamic validation. We illustrate the key results on this assertion method, including relative completeness of its proof system. and discuss its applications.
Aug 27 2010, 11:30
Speaker: Mario S. Alvim, Miguel Andres and Catuscia Palamidessi
Title: Information Hiding in Probabilistic Concurrent Systems

We consider the problem of defining the information leakage in interactive systems where secrets and observables can alternate during the computation.

We show that the information-theoretic approach which interprets such systems as (simple) noisy channels is not valid anymore. However, the principle can be recovered if we consider more complicated types of channels, that in Information Theory are known as channels with memory and feedback. We show that there is a complete correspondence between interactive systems and such kind of channels. Furthermore, we show that the capacity of the channels associated to such systems is a continuous function of the Kantorovich metric.

Aug 27 2010, 10:30
Speaker: Pierre-Malo Denielou
Title: Parameterised Multiparty Session Types

For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. In this talk, we introduce a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Godel's System T to express a wide range of communication patterns while keeping type checking decidable. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.
Jul 01 2010, 10:30
Speaker: Carroll Morgan
Title: Noninterference, probability, Bayes Risk and compositionality

I will outline our recent work in probabilistic noninterference, concentrating specifically on our novel definition of secure (noninterference) program refinement and its relation to Bayes Risk and other entropy-like measures.

In our approach, rather than evaluate a program's security in isolation we compare two programs --a specification S, and a purported implementation I-- to see whether the latter is at least as secure as the former. If that is so, and if as well the functional behaviour of I is the same as S (or better), then we say that S is =refined= by I.

For refinement to be useful in practice, it must be at least a pre-order between programs and it must be monotonic with respect to program contexts (a precongruence). Unfortunately, many entropy-like measures when applied to program pairs turn out not to be pre-congruences: for example it might well be that the Shannon entropy of probabilistic program S's hidden state is less than that entropy for I, but still there could be a context C so that for C(S) and C(I) the relation is reversed. Our refinement relation however has the property that if S is refined by I then not only is C(S) refined by C(I) for all contexts C, but also the various entropies are properly related: in this case, we would have that the Shannon entropy of C(I) is at least the entropy of C(S), and the same for the other entropies too. We call this property 'soundess' (of refinement with respect to an entropy).

But for Bayes Risk in particular we have a stronger property as well, that our refinement is its compositional closure. This is implied by our having proved it to be complete (as well as sound): that if S is -not- refined by I then there is some context C such that C(I) is strictly worse than C(S) according to Bayes Risk. This means immediately that Bayes Risk with contexts is at least as discriminating as any other entropy measure for which refinement is sound.

Still open is whether our refinement relation is complete for other entropy measures as well and, if it isn't, what their compositional closures might be instead.

Background publications:

[1] Compositional closure for Bayes Risk in probabilistic noninterference. Annabelle McIver, Larissa Meinicke and Carroll Morgan. (To appear in Proc ICALP 2010.) -> Publications -> Information Security and Anonymity -> [McIver:10]

[2] The Shadow Knows: Refinement of ignorance in sequential programs. Carroll Morgan. In LNCS 4014 Proc. MPC 2006, Tarmo Uustalu (ed.) 2006. [3] The Shadow Knows: Refinement of ignorance in sequential programs. Carroll Morgan. In Science of Computer Programming 74(8), 2009. [4] Sums and lovers: Case studies in security, compositionality and refinement. McIver, Morgan. Proc. FM09, LNCS 5850, Cavalcanti, Dams (eds.) 2009. [5] Security, probability and nearly fair coins in the cryptographers' café. McIver, Meinicke and Morgan. Invited talk in Proc. FM09, LNCS 5850, Cavalcanti, Dams (eds.) 2009.

May 28 2010, 14:30
Speaker: Luis Fernando Pino
Title: Basic Concepts on Well Structured Transition Systems

Finkel et al. defined Well Structured Transitions Systems (WSTS's) as a general class of infinite state systems which have several decidability results. They rely on the existence of a well-quasi-order given in terms of the states which is compatible with the transition relation of the system. In this talk we will present the basics concepts behind WSTS's and its application to well known formalisms like: Petri Nets, String Rewriting, BPA's. The concepts presented here were taken from the work of A. Finkel, P. Schnobelen and P. Abdulla [1][2][3].

[1] A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere!. Theoretical Computer Science, 256(1-2):63{92, Apr. 2001. [2] P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput., 160(1-2):109{127, 2000. [3] A. Finkel and Ph. Schnoebelen. Fundamental structures in well-structured infinite transition systems. In C. L. Lucchesi and A. V. Moura, editors, Proceedings of the 3rd Latin American Symposium on Theoretical Informatics (LATIN'98), volume 1380 of Lecture Notes in Computer Science, pages 102{118, Campinas, Brasil, Apr. 1998. Springer.

Apr 27 2010, 10:00
Speaker: Jan Rutten, Filippo Bonchi and Ivan Gazeau
Title: (Linear) Weighted Automata, algorithms and an application for bounding errors


Apr 26 2010, 14:30
Speaker: Alexandra Silva and Marcello Bonsangue
Title: Adding expressivity to Coalgebra Theory: all the equivalences of FT-coalgebras!!!


Apr 26 2010, 10:00
Speaker: Catuscia Palamidessi and Mario Alvim
Title: From Information Theory to Kantorovich Metric: an application to anonimity and leakage


Mar 23 2010, 10:30
Speaker: Jeremy Avigad
Title: Decision procedures, heuristic procedures, and formally verified mathematics

I will describe a mixed-bag of decidability results, some practical, and some not, loosely related to problems that arise in the formal verification of mathematics. First, I will discuss a decision procedure for a fragment of a theory of asymptotic 'big O' equations. Next, I will Nelson-Oppen combination methods in the context of theories of the real numbers. Finally, I will discuss the geometric proofs one finds in Euclid's *Elements*, and procedures that 'read information off from the diagram.'

(These various projects involve joint work with Ed Dean, Kevin Donnelly, Harvey Friedman, and John Mumma).

Mar 10 2010, 15:00
Speaker: Cienzia Di Giusto
Title: On the Computational Strenght of Higher Order and Passivation

In higher-order process calculi the values exchanged in communications may contain processes. There are only two capabilities for received processes: execution and forwarding. Here we propose a limited form of forwarding: output actions can only communicate the parallel composition of statically known closed processes and processes received through previously executed input actions.

We study the expressiveness of a higher-order process calculus featuring this style of communication. Our main result shows that in this calculus termination is decidable while convergence is undecidable. Then, as a way of recovering the expressiveness loss due to limited forwarding, we extend the calculus with a form of process suspension called passivation. Somewhat surprisingly, in the calculus extended with passivation both termination and convergence are undecidable.

Finally we present an hierarchy of languages to discuss how the presence/absence of higher order capabilities and passivation affects the expressive power of a language.

Mar 04 2009, 14:30
Speaker: Andrew Gacek
Title: A Framework for Specification, Prototyping, and Reasoning

This talk focuses on the specification of and reasoning about formal systems such as type assignment and evaluation semantics in programming languages. I introduce a logic which allows key aspects of such systems, including variable binding structure within the objects they deal with, to be specified directly and which allows reasoning to be performed over these specifications. Many of these reasoning tasks inductively analyze the structure of terms by instantiating bound variables with fresh free variables. I show how this can be captured in a logical setting through a process of moving binding from the term level to the proof level. It is often necessary in reasoning to be able to identify occurrences of variables captured by such proof level binders and to be able to distinguish between variable occurrences governed by different binders. I describe a new logical device that is capable of capturing such rich properties about binding, and I show how this device can naturally encode informal arguments based on free variable occurrences. Stepping back, I show how many similar features of specifications can be abstracted out by using an intermediate specification logic. I briefly describe how this intermediate specification logic can be given an operational semantics so that specifications can be animated automatically, and I explain how the specification logic can be exploited during reasoning to yield many interesting theorems "for free". Finally, I discuss the implementation of these ideas in the Abella theorem proving system and describe the applications of it that I have explored thus far.

Page maintainer: Carlos Olarte