School of Electronic Engineering and Computer Science

Professor Dino Distefano


Professor of Software Verification

Telephone: +44 20 7882 8794
Room Number: Peter Landin, CS 430
Office Hours: Monday 11:00-12:00


Research Interests:

I?m mainly interested in automatic program verification. In particular I focus on the application of separation logic as a main tool for modular program analysis and model checking of software.


  • MALACARIA P, TAUTCHNING M, DISTEFANO D (2016). Information leakage analysis of complex C code and its application to OpenSSL. 7th International Symposium on Leveraging Applications
  • Calcagno C, Distefano D, Dubreil J et al. (2015). Moving Fast with Software Verification. nameOfConference
  • Distefano D, Dubreil J (2013). Detecting Data Races on OpenCL Kernels with Symbolic Execution.. nameOfConference
  • Grigore R, Distefano D, Petersen RL et al. (2013). Runtime Verification Based on Register Automata. nameOfConference
  • Distefano D (2012). A Voyage to the Deep-Heap. 19th International Symposium, SAS 2012
  • Dias RJ, Distefano D, Seco JAC et al. (2012). Verification of Snapshot Isolation in Transactional Memory Java Programs. nameOfConference
  • Calcagno C, Distefano D, O'Hearn PW et al. (2011). Compositional Shape Analysis by Means of Bi-Abduction. nameOfConference
  • DISTEFANO D, Brotherston J, Petersen R (2011). Automated Cyclic Entailment Proofs in Separation Logic. CADE-23 - 23rd International Conference on Automated Deduction
  • Bormer T, Brockschmidt M, Distefano D et al. (2011). The COST IC0701 Verification Competition 2011.. nameOfConference
  • Naudziuniene D, Botincan M, Distefano D et al. (2011). jStar-eclipse: an IDE for automated verification of Java programs. nameOfConference
  • DISTEFANO D, Filipovic I (2010). Memory Leaks Detection in Java by Bi- Abductive Inference. FASE 2010
  • DISTEFANO D (2009). Attacking Large Industrial Code with Bi-abductive Inference. Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems
  • DISTEFANO D, Cristiano C, Vafeiadis V (2009). Bi-abductive Resource Invariant Synthesis. Programming Languages and Systems, 7th Asian Symposium, APLAS 2009
  • Calcagno C, Distefano D, O'Hearn PW et al. (2009). Compositional shape analysis by means of bi-abduction. The 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009)
  • Calcagno C, Distefano D, O'Hearn P et al. (2009). Space Invading Systems Code. nameOfConference
  • Distefano D (2008). Abductive Inference for Reasoning about Heaps. nameOfConference
  • Yang H, Lee O, Berdine J et al. (2008). Scalable shape analysis for systems code. nameOfConference
  • Distefano D, Parkinson MJ (2008). jStar: Towards Practical Verification for Java. nameOfConference
  • Calcagno C, Distefano D, O'Hearn PW et al. (2007). Footprint Analysis: A Shape Analysis that Discovers Preconditions. The 14th International Static Analysis Symposium (SAS 2007)
  • Berdine J, Calcagno C, Cook B et al. (2007). Shape analysis for composite data structures. nameOfConference
  • Berdine J, Chawdhary A, Cook B et al. (2007). Variance Analyses from Invariance Analyses. nameOfConference
  • Berdine J, Chawdhary A, Cook B et al. (2007). Variance analyses from invariance analyses. nameOfConference
  • Distefano D, O'Hearn PW, Yang H (2006). A local shape analysis based on separation logic. nameOfConference
  • Rensink A, Distefano D (2006). Abstract Graph Transformation.. nameOfConference
  • Berdine J, Cook B, Distefano D et al. (2006). Automatic termination proofs for programs with shape-shifting heaps. nameOfConference
  • Calcagno C, Distefano D, O'Hearn PW et al. (2006). Beyond reachability: Shape abstraction in the presence of pointer arithmetic. nameOfConference
  • Distefano D, Katoen JP, Rensink A (2006). Safety and liveness in concurrent pointer programs. nameOfConference
  • Distefano D (2005). A parametric model for the analysis of mobile ambients. nameOfConference
  • Distefano D, Katoen J-P, Rensink A (2004). Who is Pointing When to Whom?. nameOfConference
  • Distefano D, Katoen JP, Rensink A (2004). Who is pointing when to whom? On the automated verification of linked list structures. nameOfConference
  • Distefano D, Rensink A, Katoen JP (2002). Model checking birth and death. nameOfConference