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 Fundamentals of AI and Computational Theory2024
Enhancing Compositional Static Analysis with Dynamic AnalysisDistefano D Marescotti M Ahs C Cela S Grigore R Hajdu A
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
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 Harman M
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
In Static Analysis, Springer Nature 3-6.
01-01-2020
2019
Scaling Static Analyses at FacebookDistefano D Fahndrich M 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 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 O’Hearn P Purbrick J
Lecture Notes in Computer Science. vol. 9058, 3-11.
01-01-2015
2013
Detecting Data Races on OpenCL Kernels with Symbolic Execution.Distefano D Dubreil J
Corr vol. abs/1308.3203
01-01-2013
2012
Runtime Verification Based on Register AutomataGrigore R Distefano D 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 Seco JAC
ECOOP., 640-664-640-664.
01-01-2012
2011
Compositional Shape Analysis by Means of Bi-AbductionCalcagno C Distefano D O'Hearn PW
Journal of The Acm vol. 58 (6)
01-12-2011
Automated Cyclic Entailment Proofs in Separation LogicDISTEFANO D Petersen R Bjørner N Sofronie-Stokkermans V
CADE-23 - 23rd International Conference on Automated Deduction., 131-146.
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 et al.
FoVeOOS. vol. 7421, 3-21.
01-01-2011
jStar-eclipse: an IDE for automated verification of Java programsNaudziuniene D Botincan M Distefano D Grigore R
SIGSOFT FSE., 428-431-428-431.
01-01-2011
2010
Memory Leaks Detection in Java by Bi-
Abductive InferenceDISTEFANO D 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 Yang H Hanus M
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION. vol. 5438, 1-3.
01-01-2009
Compositional shape analysis by means of bi-abductionCalcagno C Distefano D O'Hearn PW
The 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009) Savannah, GA, USA 21 Jan 2009 - 23 Jan 2009., 289-300.
01-01-2009
Bi-abductive Resource Invariant SynthesisDISTEFANO D Cristiano C
Programming Languages and Systems, 7th Asian Symposium, APLAS 2009 Tokyo, Japan 1 Jan 1970. vol. 5904}
01-01-2009
2008
Abductive Inference for Reasoning about HeapsDistefano D Ramalingam G
PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS. vol. 5356, 1-2.
01-01-2008
Scalable shape analysis for systems codeYang H Lee O Berdine J Cook B Distefano D Gupta A Malik S
COMPUTER AIDED VERIFICATION. vol. 5123, 385-398.
01-01-2008
jStar: Towards Practical Verification for JavaDistefano D Parkinson MJ
OOPSLA 2008 NASHVILLE, CONFERENCE PROCEEDINGS., 213-226.
01-01-2008
2007
Shape analysis for composite data structuresBerdine J Calcagno C Cook B O'Hearn PW Wies T Damm W Hermanns H
Computer Aided Verification, Proceedings. vol. 4590, 178-192.
01-01-2007
Variance analyses from invariance analysesBerdine J Chawdhary A Distefano D
ACM SIGPLAN NOTICES. vol. 42 (1), 211-224.
01-01-2007
Variance Analyses from Invariance AnalysesBerdine J Chawdhary A Distefano D
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 Yang H Nielson HR 'e GF
The 14th International Static Analysis Symposium (SAS 2007) Kongens Lyngby, Denmark 22 Aug 2007 - 24 Aug 2007. vol. 4634, 402-418.
01-01-2007
2006
Safety and liveness in concurrent pointer programsDistefano D Katoen JP DeBoer FS Bonsangue MM Graf S DeRoever WP
FORMAL METHODS FOR COMPONENTS AND OBJECTS. vol. 4111, 280-312.
01-01-2006
A local shape analysis based on separation logicDistefano D O'Hearn PW Yang H Hermanns H Palsberg J
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS. vol. 3920, 287-302.
01-01-2006
Beyond reachability: Shape abstraction in the presence of pointer arithmeticCalcagno C Distefano D O'Hearn PW Kwangkeun Y
STATIC ANALYSIS, PROCEEDINGS. vol. 4134, 182-203.
01-01-2006
Automatic termination proofs for programs with shape-shifting heapsBerdine J Cook B O'Hearn PW Ball T Jones RB
COMPUTER AIDED VERIFICATION, PROCEEDINGS. vol. 4144, 386-400.
01-01-2006
2005
Abstract Graph Transformation.Rensink A Distefano D Mukhopadhyay S Roychoudhury A Yang Z
Svv@Icfem, Elsevier vol. 157, 39-59.
01-01-2005
A parametric model for the analysis of mobile ambientsDistefano D Yi K
PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS. vol. 3780, 401-417.
01-01-2005
2004
Who is pointing when to whom? On the automated verification of linked list structuresDistefano D Katoen JP Rensink A Lodaya K Mahajan M
FSTTCS 2004: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE. vol. 3328, 250-262.
01-01-2004
Who is Pointing When to Whom?Distefano D Katoen J-P Lodaya K Mahajan M
FSTTCS. vol. 3328, 250-262.
01-01-2004
2002
Model checking birth and deathDistefano D Rensink A BaezaYates R Montanari U Santoro N
FOUNDATIONS OF INFORMATION TECHNOLOGY IN THE ERA OF NETWORK AND MOBILE COMPUTING. vol. 96, 435-447.
01-01-2002
2000
On a Temporal Logic for Object-Based SystemsDistefano D Katoen J-P
IFIP Advances in Information and Communication Technology. vol. 49, 305-325.
01-01-2000
Automatic Compositional Checking of Multi-Object TypeState Properties of SoftwareGrigore R Distefano D Tzevelekos N
Principles of Verification: Cycling The Probabilistic Landscape
Research Group
News
No news items found.