Professor Dino Distefano

Research

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.

Publications

• Mao K, Kapus T, Petrou L et al. (2022). FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsApp. nameOfConference

  
  

  DOI: 10.1109/ICST53961.2022.00036

  
  

  QMRO: qmroHref
• Çiçek E, Bouaziz M, Cho S et al. (2020). Static Resource Analysis at Scale (Extended Abstract). nameOfConference

  
  

  DOI: 10.1007/978-3-030-65474-0_1

  
  

  QMRO: qmroHref
• Distefano D, Fahndrich M, Logozzo F et al. (2019). Scaling Static Analyses at Facebook. nameOfConference

  
  

  DOI: 10.1145/3338112

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/61979
• 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

  
  

  DOI: 10.1007/978-3-319-47166-2_63

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13880
• Calcagno C, Distefano D, Dubreil J et al. (2015). Moving fast with software verification. nameOfConference

  
  

  DOI: 10.1007/978-3-319-17524-9_1

  
  

  QMRO: qmroHref
• Distefano D, Dubreil J (2013). Detecting Data Races on OpenCL Kernels with Symbolic Execution.. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Grigore R, Distefano D, Petersen RL et al. (2012). Runtime Verification Based on Register Automata. nameOfConference

  
  

  DOI: 10.1007/978-3-642-36742-7_19

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/19031
• Distefano D (2012). A Voyage to the Deep-Heap. 19th International Symposium, SAS 2012

  
  

  DOI: 10.1007/978-3-642-33125-1_2

  
  

  QMRO: qmroHref
• Dias RJ, Distefano D, Seco JAC et al. (2012). Verification of Snapshot Isolation in Transactional Memory Java Programs. nameOfConference

  
  

  DOI: 10.1007/978-3-642-31057-7_28

  
  

  QMRO: qmroHref
• Calcagno C, Distefano D, O'Hearn PW et al. (2011). Compositional Shape Analysis by Means of Bi-Abduction. nameOfConference

  
  

  DOI: 10.1145/2049697.2049700

  
  

  QMRO: qmroHref
• DISTEFANO D, Brotherston J, Petersen R (2011). Automated Cyclic Entailment Proofs in Separation Logic. CADE-23 - 23rd International Conference on Automated Deduction

  
  

  DOI: 10.1007/978-3-642-22438-6_12

  
  

  QMRO: qmroHref
• Bormer T, Brockschmidt M, Distefano D et al. (2011). The COST IC0701 Verification Competition 2011.. nameOfConference

  
  

  DOI: 10.1007/978-3-642-31762-0_2

  
  

  QMRO: qmroHref
• Naudziuniene D, Botincan M, Distefano D et al. (2011). jStar-eclipse: an IDE for automated verification of Java programs. nameOfConference

  
  

  DOI: 10.1145/2025113.2025182

  
  

  QMRO: qmroHref
• DISTEFANO D, Filipovic I (2010). Memory Leaks Detection in Java by Bi- Abductive Inference. FASE 2010

  
  

  DOI: 10.1007/978-3-642-12029-9_20

  
  

  QMRO: qmroHref
• DISTEFANO D (2009). Attacking Large Industrial Code with Bi-abductive Inference. Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems

  
  

  DOI: 10.1007/978-3-642-04570-7_1

  
  

  QMRO: qmroHref
• DISTEFANO D, Cristiano C, Vafeiadis V (2009). Bi-abductive Resource Invariant Synthesis. Programming Languages and Systems, 7th Asian Symposium, APLAS 2009

  
  

  DOI: 10.1007/978-3-642-10672-9_19

  
  

  QMRO: qmroHref
• 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)

  
  

  DOI: 10.1145/1480881.1480917

  
  

  QMRO: qmroHref
• Calcagno C, Distefano D, O'Hearn P et al. (2009). Space Invading Systems Code. nameOfConference

  
  

  DOI: 10.1007/978-3-642-00515-2_1

  
  

  QMRO: qmroHref
• Distefano D (2008). Abductive Inference for Reasoning about Heaps. nameOfConference

  
  

  DOI: 10.1007/978-3-540-89330-1_1

  
  

  QMRO: qmroHref
• Yang H, Lee O, Berdine J et al. (2008). Scalable shape analysis for systems code. nameOfConference

  
  

  DOI: 10.1007/978-3-540-70545-1_36

  
  

  QMRO: qmroHref
• Distefano D, Parkinson MJ (2008). jStar: Towards Practical Verification for Java. nameOfConference

  
  

  DOI: 10.1145/1449764.1449782

  
  

  QMRO: qmroHref
• 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)

  
  

  DOI: 10.1007/978-3-540-74061-2_25

  
  

  QMRO: qmroHref
• Berdine J, Calcagno C, Cook B et al. (2007). Shape analysis for composite data structures. nameOfConference

  
  

  DOI: 10.1007/978-3-540-73368-3_22

  
  

  QMRO: qmroHref
• Berdine J, Chawdhary A, Cook B et al. (2007). Variance Analyses from Invariance Analyses. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Berdine J, Chawdhary A, Cook B et al. (2007). Variance analyses from invariance analyses. nameOfConference

  
  

  DOI: 10.1145/1190216.1190249

  
  

  QMRO: qmroHref
• Distefano D, O'Hearn PW, Yang H (2006). A local shape analysis based on separation logic. nameOfConference

  
  

  DOI: 10.1007/11691372_19

  
  

  QMRO: qmroHref
• Rensink A, Distefano D (2006). Abstract Graph Transformation.. nameOfConference

  
  

  DOI: 10.1016/j.entcs.2006.01.022

  
  

  QMRO: qmroHref
• Berdine J, Cook B, Distefano D et al. (2006). Automatic termination proofs for programs with shape-shifting heaps. nameOfConference

  
  

  DOI: 10.1007/11817963_35

  
  

  QMRO: qmroHref
• Calcagno C, Distefano D, O'Hearn PW et al. (2006). Beyond reachability: Shape abstraction in the presence of pointer arithmetic. nameOfConference

  
  

  DOI: 10.1007/11823230_13

  
  

  QMRO: qmroHref
• Distefano D, Katoen JP, Rensink A (2006). Safety and liveness in concurrent pointer programs. nameOfConference

  
  

  DOI: 10.1007/11804192_14

  
  

  QMRO: qmroHref
• Distefano D (2005). A parametric model for the analysis of mobile ambients. nameOfConference

  
  

  DOI: 10.1007/11575467_26

  
  

  QMRO: qmroHref
• Distefano D, Katoen J-P, Rensink A (2004). Who is Pointing When to Whom?. nameOfConference

  
  

  DOI: 10.1007/978-3-540-30538-5_21

  
  

  QMRO: qmroHref
• Distefano D, Katoen JP, Rensink A (2004). Who is pointing when to whom? On the automated verification of linked list structures. nameOfConference

  
  

  DOI: 10.1007/978-3-540-30538-5_21

  
  

  QMRO: qmroHref
• Distefano D, Rensink A, Katoen JP (2002). Model checking birth and death. nameOfConference

  
  

  DOI: 10.1007/978-0-387-35608-2_36

  
  

  QMRO: qmroHref
• Distefano D, Katoen JP, Rensink A (2000). On a temporal logic for object-based systems. nameOfConference

  
  

  DOI: 10.1007/978-0-387-35520-7_16

  
  

  QMRO: qmroHref