PLUME

• Mathematical foundations for correct software
  Our research focuses on mathematical foundations for correct software with the particularity of combining expertise in ‘a priori’ methods for correctness by construction and ‘a posteriori’ methods for correctness by verification.

• Correctness by construction
  Our research in this area is deeply informed by the Curry-Howard isomorphism between proofs and programs. We build type systems to provide static guarantees for important properties of programs. We use semantics to analyse and compare sequential and concurrent programming primitives. We construct machine-assisted formalizations of mathematical theories in Coq in order to bring standard verification techniques into the realm of proof assistants.

• Correctness by verification
  Our research in this area combines traditional verification techniques with more recent developments in co-induction. We extend the scope of specification logics to probabilistic settings and higher-order model checking. We develop efficient new algorithms for proving language equivalences using ‘bisimulation up to’ techniques from process calculus. We exploit causality in graph rewriting to extract signalling pathways from simulation traces of models derived from biological knowledge.

   

Main collaborations: Bologna (Italy), Warsaw (Poland), Cambridge (UK), Harvard Medical School (USA)