Prof Dino Distefano
Professor of Software Verification
School of Electronic Engineering and Computer Science
Queen Mary University of London
Queen Mary University of London
Research
automatic program verification
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
Publications of specific relevance to the Centre for Fundamental Computer Science2024
Grigore R, Distefano D and Tzevelekos N (2024). Automatic Compositional Checking of Multi-object TypeState Properties of Software. Lecture Notes in Computer Science, Springer Nature vol. 15260, 3-40. 13-11-2024
Distefano D, Marescotti M, Ahs C, Cela S, Sampaio GC, Grigore R, Hajdu A, Kapus T, Mao K and Suzanne T (2024). Enhancing Compositional Static Analysis with Dynamic Analysis. Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. 27-10-2024
Distefano D (2024). PrivacyCAT: Privacy-Aware Code Analysis at Scale. ICSE 2024 Software Engineering in Practice When. 17-04-2024
2022
Hajdu Á, Marescotti M, Suzanne T, Mao K, Grigore R, Gustafsson P and Distefano D (2022). InfERL: scalable and extensible Erlang static analysis. Proceedings of the 21st ACM SIGPLAN International Workshop on Erlang. 06-09-2022
Mao K, Kapus T, Petrou L, Hajdu A, Marescotti M, Loscher A, Harman M and Distefano D (2022). FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsApp. 2022 IEEE Conference on Software Testing, Verification and Validation (ICST). 14-04-2022
2020
Çiçek E, Bouaziz M, Cho S and Distefano D (2020). Static Resource Analysis at Scale (Extended Abstract). Static Analysis 3-6. 01-01-2020
2019
Distefano D, Fahndrich M, Logozzo F and O'Hearn PW (2019). Scaling Static Analyses at Facebook. COMMUNICATIONS OF THE ACM vol. 62 (8), 62-70. 01-08-2019
2016
MALACARIA P, TAUTCHNING M and DISTEFANO D (2016). Information leakage analysis of complex C code and its application to OpenSSL. 7th International Symposium on Leveraging Applications CORFU 10 Oct 2016 - 14 Oct 2016. 05-10-2016
2015
Calcagno C, Distefano D, Dubreil J, Gabi D, Hooimeijer P, Luca M, O’Hearn P, Papakonstantinou I, Purbrick J and Rodriguez D (2015). Moving Fast with Software Verification. 01-01-2015
2013
Distefano D and Dubreil J (2013). Detecting Data Races on OpenCL Kernels with Symbolic Execution. CoRR vol. abs/1308.3203 01-01-2013
2012
Grigore R, Distefano D, Petersen RL and Tzevelekos N (2012). Runtime Verification Based on Register Automata. 24-09-2012
Distefano D (2012). A Voyage to the Deep-Heap. 19th International Symposium, SAS 2012 Deauville, France 11 Sep 2012 - 12 Sep 2012. 01-01-2012
Dias RJ, Distefano D, Seco JAC and Lourenço JA (2012). Verification of Snapshot Isolation in Transactional Memory Java Programs. 01-01-2012
2011
Calcagno C, Distefano D, O'Hearn PW and Yang H (2011). Compositional Shape Analysis by Means of Bi-Abduction. Journal of the ACM vol. 58 (6) 01-12-2011
DISTEFANO D, Brotherston J and Petersen R (2011). Automated Cyclic Entailment Proofs in Separation Logic., Editors: Bjørner N and Sofronie-Stokkermans V. CADE-23 - 23rd International Conference on Automated Deduction. 01-01-2011
Bormer T, Brockschmidt M, Distefano D, Ernst G, Filliâtre J-C, Grigore R, Huisman M, Klebanov V, Marché C, Monahan R, Mostowski W, Polikarpova N, Scheben C, Schellhorn G, Tofan B, Tschannen J and Ulbrich M (2011). The COST IC0701 Verification Competition 2011., Editors: Beckert B, Damiani F and Gurov D. 01-01-2011
Naudziuniene D, Botincan M, Distefano D, Dodds M, Grigore R and Parkinson MJ (2011). jStar-eclipse: an IDE for automated verification of Java programs. 01-01-2011
2010
DISTEFANO D and Filipovic I (2010). Memory Leaks Detection in Java by Bi-
Abductive Inference. FASE 2010. 01-01-2010
2009
DISTEFANO D (2009). Attacking Large Industrial Code with Bi-abductive Inference. Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems Berlin. 01-01-2009
Calcagno C, Distefano D, O'Hearn P and Yang H (2009). Space Invading Systems Code., Editors: Hanus M. 01-01-2009
Calcagno C, Distefano D, O'Hearn PW and Yang H (2009). Compositional shape analysis by means of bi-abduction., Editors: Shao Z and Pierce BC. The 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009) Savannah, GA, USA 21 Jan 2009 - 23 Jan 2009. 01-01-2009
DISTEFANO D, Cristiano C and Vafeiadis V (2009). Bi-abductive Resource Invariant Synthesis., Editors: Hu Z. Programming Languages and Systems, 7th Asian Symposium, APLAS 2009 Tokyo, Japan 1 Jan 1970. 01-01-2009
2008
Distefano D (2008). Abductive Inference for Reasoning about Heaps., Editors: Ramalingam G. 01-01-2008
Yang H, Lee O, Berdine J, Calcagno C, Cook B, Distefano D and O'Hearn P (2008). Scalable shape analysis for systems code., Editors: Gupta A and Malik S. 01-01-2008
2007
Berdine J, Calcagno C, Cook B, Distefano D, O'Hearn PW, Wies T and Yang HS (2007). Shape analysis for composite data structures., Editors: Damm W and Hermanns H. 01-01-2007
Berdine J, Chawdhary A, Cook B, Distefano D and O'Hearn P (2007). Variance analyses from invariance analyses. 01-01-2007
Berdine J, Chawdhary A, Cook B, Distefano D and O'Hearn P (2007). Variance Analyses from Invariance Analyses. 01-01-2007
Calcagno C, Distefano D, O'Hearn PW and Yang H (2007). Footprint Analysis: A Shape Analysis that Discovers Preconditions., Editors: Nielson HR and 'e GF. The 14th International Static Analysis Symposium (SAS 2007) Kongens Lyngby, Denmark 22 Aug 2007 - 24 Aug 2007. 01-01-2007
2006
Distefano D, Katoen JP and Rensink A (2006). Safety and liveness in concurrent pointer programs., Editors: DeBoer FS, Bonsangue MM, Graf S and DeRoever WP. 01-01-2006
Distefano D, O'Hearn PW and Yang H (2006). A local shape analysis based on separation logic., Editors: Hermanns H and Palsberg J. 01-01-2006
Calcagno C, Distefano D, O'Hearn PW and Yang H (2006). Beyond reachability: Shape abstraction in the presence of pointer arithmetic., Editors: Kwangkeun Y. 01-01-2006
Berdine J, Cook B, Distefano D and O'Hearn PW (2006). Automatic termination proofs for programs with shape-shifting heaps., Editors: Ball T and Jones RB. 01-01-2006
2005
Rensink A and Distefano D (2005). Abstract Graph Transformation., Editors: Mukhopadhyay S, Roychoudhury A and Yang Z. SVV@ICFEM, Elsevier vol. 157, 39-59. 01-01-2005
Distefano D (2005). A parametric model for the analysis of mobile ambients., Editors: Yi K. 01-01-2005
2004
Distefano D, Katoen JP and Rensink A (2004). Who is pointing when to whom? On the automated verification of linked list structures., Editors: Lodaya K and Mahajan M. 01-01-2004
Distefano D, Katoen J-P and Rensink A (2004). Who is Pointing When to Whom?, Editors: Lodaya K and Mahajan M. 01-01-2004
2002
Distefano D, Rensink A and Katoen JP (2002). Model checking birth and death., Editors: BaezaYates R, Montanari U and Santoro N. 01-01-2002
2000
Distefano D, Katoen J-P and Rensink A (2000). On a Temporal Logic for Object-Based Systems. 01-01-2000