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
Automatic Compositional Checking of Multi-object TypeState Properties of SoftwareGrigore R, Distefano D and Tzevelekos N
Lecture Notes in Computer Science, Springer Nature vol. 15260, 3-40.
13-11-2024
Enhancing Compositional Static Analysis with Dynamic AnalysisDistefano D, Marescotti M, Ahs C, Cela S, Sampaio GC, Grigore R, Hajdu A, Kapus T, Mao K and Suzanne T
Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering., 2121-2129.
27-10-2024
PrivacyCAT: Privacy-Aware Code Analysis at ScaleDistefano D
ICSE 2024 Software Engineering in Practice When.
17-04-2024
2022
InfERL: scalable and extensible Erlang static analysisHajdu Á, Marescotti M, Suzanne T, Mao K, Grigore R, Gustafsson P and Distefano D
Proceedings of the 21st ACM SIGPLAN International Workshop on Erlang., 33-39.
06-09-2022
FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsAppMao K, Kapus T, Petrou L, Hajdu A, Marescotti M, Loscher A, Harman M and Distefano D
2022 IEEE Conference on Software Testing, Verification and Validation (ICST). vol. 00, 267-278.
14-04-2022
2020
Static Resource Analysis at Scale (Extended Abstract)Çiçek E, Bouaziz M, Cho S and Distefano D
In Static Analysis, Springer Nature 3-6.
01-01-2020
2019
Scaling Static Analyses at FacebookDistefano D, Fahndrich M, Logozzo F and O'Hearn PW
Communications of The Acm vol. 62 (8), 62-70.
01-08-2019
2016
Information leakage analysis of complex C code and its application to OpenSSLMALACARIA P, TAUTCHNING M and DISTEFANO D
7th International Symposium on Leveraging Applications CORFU 10 Oct 2016 - 14 Oct 2016.
05-10-2016
2015
Moving Fast with Software VerificationCalcagno C, Distefano D, Dubreil J, Gabi D, Hooimeijer P, Luca M, O’Hearn P, Papakonstantinou I, Purbrick J and Rodriguez D
Lecture Notes in Computer Science. vol. 9058, 3-11.
01-01-2015
2013
Detecting Data Races on OpenCL Kernels with Symbolic Execution.Distefano D and Dubreil J
Corr vol. abs/1308.3203
01-01-2013
2012
Runtime Verification Based on Register AutomataGrigore R, Distefano D, Petersen RL and Tzevelekos N
24-09-2012
A Voyage to the Deep-HeapDistefano D
19th International Symposium, SAS 2012 Deauville, France 11 Sep 2012 - 12 Sep 2012., 3-3.
01-01-2012
Verification of Snapshot Isolation in Transactional Memory Java ProgramsDias RJ, Distefano D, Seco JAC and Lourenço JA
ECOOP., 640-664-640-664.
01-01-2012
2011
Compositional Shape Analysis by Means of Bi-AbductionCalcagno C, Distefano D, O'Hearn PW and Yang H
Journal of The Acm vol. 58 (6)
01-12-2011
Automated Cyclic Entailment Proofs in Separation LogicDISTEFANO D, Brotherston J and Petersen R
CADE-23 - 23rd International Conference on Automated Deduction., 131-146. Editors: Bjørner N and Sofronie-Stokkermans V.
01-01-2011
The COST IC0701 Verification Competition 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
FoVeOOS. vol. 7421, 3-21. Editors: Beckert B, Damiani F and Gurov D.
01-01-2011
jStar-eclipse: an IDE for automated verification of Java programsNaudziuniene D, Botincan M, Distefano D, Dodds M, Grigore R and Parkinson MJ
SIGSOFT FSE., 428-431-428-431.
01-01-2011
2010
Memory Leaks Detection in Java by Bi-
Abductive InferenceDISTEFANO D and Filipovic I
FASE 2010. vol. 6013, 278-292.
01-01-2010
2009
Attacking Large Industrial Code with Bi-abductive InferenceDISTEFANO D
Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems Berlin. vol. 5825
01-01-2009
Space Invading Systems CodeCalcagno C, Distefano D, O'Hearn P and Yang H
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION. vol. 5438, 1-3. Editors: Hanus M.
01-01-2009
Compositional shape analysis by means of bi-abductionCalcagno C, Distefano D, O'Hearn PW and Yang H
The 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009) Savannah, GA, USA 21 Jan 2009 - 23 Jan 2009., 289-300. Editors: Shao Z and Pierce BC.
01-01-2009
Bi-abductive Resource Invariant SynthesisDISTEFANO D, Cristiano C and Vafeiadis V
Programming Languages and Systems, 7th Asian Symposium, APLAS 2009 Tokyo, Japan 1 Jan 1970. vol. 5904} Editors: Hu Z.
01-01-2009
2008
Abductive Inference for Reasoning about HeapsDistefano D
PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS. vol. 5356, 1-2. Editors: Ramalingam G.
01-01-2008
Scalable shape analysis for systems codeYang H, Lee O, Berdine J, Calcagno C, Cook B, Distefano D and O'Hearn P
COMPUTER AIDED VERIFICATION. vol. 5123, 385-398. Editors: Gupta A and Malik S.
01-01-2008
jStar: Towards Practical Verification for JavaDistefano D and Parkinson MJ
OOPSLA 2008 NASHVILLE, CONFERENCE PROCEEDINGS., 213-226.
01-01-2008
2007
Shape analysis for composite data structuresBerdine J, Calcagno C, Cook B, Distefano D, O'Hearn PW, Wies T and Yang HS
Computer Aided Verification, Proceedings. vol. 4590, 178-192. Editors: Damm W and Hermanns H.
01-01-2007
Variance analyses from invariance analysesBerdine J, Chawdhary A, Cook B, Distefano D and O'Hearn P
ACM SIGPLAN NOTICES. vol. 42 (1), 211-224.
01-01-2007
Variance Analyses from Invariance AnalysesBerdine J, Chawdhary A, Cook B, Distefano D and O'Hearn P
CONFERENCE RECORD OF POPL 2007: THE 34TH ACM SIGPLAN SIGACT SYMPOSIUM ON PRINCIPLES OF PROGAMMING LANGUAGES., 211-224.
01-01-2007
Footprint Analysis: A Shape Analysis that Discovers PreconditionsCalcagno C, Distefano D, O'Hearn PW and Yang H
The 14th International Static Analysis Symposium (SAS 2007) Kongens Lyngby, Denmark 22 Aug 2007 - 24 Aug 2007. vol. 4634, 402-418. Editors: Nielson HR and 'e GF.
01-01-2007
2006
Safety and liveness in concurrent pointer programsDistefano D, Katoen JP and Rensink A
FORMAL METHODS FOR COMPONENTS AND OBJECTS. vol. 4111, 280-312. Editors: DeBoer FS, Bonsangue MM, Graf S and DeRoever WP.
01-01-2006
A local shape analysis based on separation logicDistefano D, O'Hearn PW and Yang H
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS. vol. 3920, 287-302. Editors: Hermanns H and Palsberg J.
01-01-2006
Beyond reachability: Shape abstraction in the presence of pointer arithmeticCalcagno C, Distefano D, O'Hearn PW and Yang H
STATIC ANALYSIS, PROCEEDINGS. vol. 4134, 182-203. Editors: Kwangkeun Y.
01-01-2006
Automatic termination proofs for programs with shape-shifting heapsBerdine J, Cook B, Distefano D and O'Hearn PW
COMPUTER AIDED VERIFICATION, PROCEEDINGS. vol. 4144, 386-400. Editors: Ball T and Jones RB.
01-01-2006
2005
Abstract Graph Transformation.Rensink A and Distefano D
Svv@Icfem, Elsevier vol. 157, 39-59. Editors: Mukhopadhyay S, Roychoudhury A and Yang Z.
01-01-2005
A parametric model for the analysis of mobile ambientsDistefano D
PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS. vol. 3780, 401-417. Editors: Yi K.
01-01-2005
2004
Who is pointing when to whom? On the automated verification of linked list structuresDistefano D, Katoen JP and Rensink A
FSTTCS 2004: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE. vol. 3328, 250-262. Editors: Lodaya K and Mahajan M.
01-01-2004
Who is Pointing When to Whom?Distefano D, Katoen J-P and Rensink A
FSTTCS. vol. 3328, 250-262. Editors: Lodaya K and Mahajan M.
01-01-2004
2002
Model checking birth and deathDistefano D, Rensink A and Katoen JP
FOUNDATIONS OF INFORMATION TECHNOLOGY IN THE ERA OF NETWORK AND MOBILE COMPUTING. vol. 96, 435-447. Editors: BaezaYates R, Montanari U and Santoro N.
01-01-2002
2000
On a Temporal Logic for Object-Based SystemsDistefano D, Katoen J-P and Rensink A
IFIP Advances in Information and Communication Technology. vol. 49, 305-325.
01-01-2000