Professor Dino DistefanoProfessor of Software VerificationEmail: d.distefano@qmul.ac.ukTelephone: +44 20 7882 8794Room Number: Peter Landin, CS 430Website: http://www.eecs.qmul.ac.uk/~ddinoOffice Hours: Monday 11:00-12:00ResearchPublicationsResearchResearch 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 Distefano D (2024). PrivacyCAT: Privacy-Aware Code Analysis at Scale. ICSE 2024 Software Engineering in Practice When DOI: 10.1145/3639477.3639742 QMRO: qmroHref Hajdu Á, Marescotti M, Suzanne T et al. (2022). InfERL: scalable and extensible Erlang static analysis. Proceedings of the 21st ACM SIGPLAN International Workshop on Erlang DOI: 10.1145/3546186.3549929 QMRO: qmroHref Mao K, Kapus T, Petrou L et al. (2022). FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsApp. 2022 IEEE Conference on Software Testing, Verification and Validation (ICST) DOI: 10.1109/icst53961.2022.00036 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/96953 Ç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://uat2-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://uat2-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://uat2-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 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 Rensink A, Distefano D (2005). Abstract Graph Transformation.. nameOfConference DOI: 10.1016/j.entcs.2006.01.022 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 J-P, Rensink A (2000). On a Temporal Logic for Object-Based Systems. nameOfConference DOI: 10.1007/978-0-387-35520-7_16 QMRO: qmroHref