Barnaby Martin gave the recent Séminaire d’algorithmique et de complexité du plateau de Saclay on the 14th December 2012. It was hosted by the École Polytechnique near Paris, in their new Bâtiment Alan Turing. The topic was “Distance Constraint Satisfaction Problems”.

Kohei Honda, our friend and colleague, passed away on December 3, 2012. He was an original thinker, always effusive and enthusiastic. Hopefully, he is in a better place already arguing with Robin Milner.
We will miss Kohei.

On November 13th, Rajagopal Nagarajan gave a seminar titled “Formal Methods  for Quantum Information Science” at the Department of Computer Science, University  of Liverpool. The talk was an overview of ongoing work in using techniques from process calculus and model-checking for the specification and verification of quantum protocols.

Christmas is less than a month away. With your friends Bob and Charlie you decide that this year it would be nice to have a Secret Santa (http://en.wikipedia.org/wiki/Secret_Santa).

However, you immediately realize that there is no way for three people to exchange gifts anonymously! If you buy a gift for Bob, you also know that Bob will buy a gift for Charlie, and that Charlie will buy your gift.

With four friends (and a complete graph whose edges represent possible exchanges) a solution seems possible. But if you start removing edges you could obtain a graph for which no solution guarantees anonymity…

How do you formally define anonymity in a graph? and how do you check if a graph has this property? what is the complexity of this problem? This paper, recently and timely accepted for publication in Elsevier Computers and Operations Research, investigates the problem:

• A. Bettinelli, L. Liberti, F. Raimondi, D. Savourey, The Anonymous Subgraph Problem, to appear in Computers & Operations Research, Elsevier (PDF preprint here).

The paper shows that, in addition to Secret Santa, this problem has practical applications in networking and routing, and in the study of vehicular networks.

On November 20 Franco Raimondi gave a talk at University of Liverpool about his work on verification of multi-agent systems in collaboration with NASA Ames. The talk was an overview of a novel approach to verify human-computer interactions specified in Brahms using Java Pathfinder and other model checkers such as SPIN, NuSMV, and PRISM.

In the MDX school seminar on 7th November, Florian Kammueller presented his work on Security of Active Objects. This talk presented the Semi-Lattice Model for Multi-Lateral Security designed for Privacy of Active Objects as recently presented at the DPM workshop at ESORICS’12. Florian also gave an overview of his ongoing work on formalisation of an information flow type system for ASPfun formalized in Isabelle/HOL.

On October 26, Jaap Boender gave a talk in the combined ToC/AI seminar, titled “Formalisation of a theory of packages in Coq”. This was an introduction to theorem proving in general and the Coq proof assistant in particular, through the formalisation of a simple theory of open source distributions, packages and the dependency and conflict relations between them.

Welcome to our webpage. This is our first item, please stay tuned for more.