Skip to main content
Research
  1. Queen Mary University of London
  2. Research
  3. Publications

Publications: Prof Dino Distefano

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