Abstracts
Nov 29 2010, 10:30
Speaker: Rohit Chadha
Title: Model Checking Concurrent Programs with Nondeterminism and Randomization
Abstract:
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
Abstract:
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
Abstract:
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
Abstract:
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
Abstract:
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
Abstract:
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
Abstract:
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
Abstract:
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.)
www.cse.unsw.edu.au/~carrollm/probs -> 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
Abstract:
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
Abstract:
Apr 26 2010, 14:30
Speaker: Alexandra Silva and Marcello Bonsangue
Title: Adding expressivity to Coalgebra Theory: all the equivalences of FT-coalgebras!!!
Abstract:
Apr 26 2010, 10:00
Speaker: Catuscia Palamidessi and Mario Alvim
Title: From Information Theory to Kantorovich Metric: an application to anonimity and leakage
Abstract:
Mar 23 2010, 10:30
Speaker: Jeremy Avigad
Title: Decision procedures, heuristic procedures, and formally verified mathematics
Abstract:
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
Abstract:
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
Abstract:
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.
|