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 Theory
2024
Automatic Compositional Checking of Multi-object TypeState Properties of SoftwareGrigore R Distefano D
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 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 ScaleMao K Åhs C Cela S Distefano D Gardner N Grigore R Hajdu Á Kapus T et al.
Proceedings of the 46th International Conference on Software Engineering: Software Engineering in Practice., 106-117.
14-04-20242022
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
Lecture Notes in Computer Science. vol. 9952, 909-925.
01-01-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
