Research menu
Jump to menu

Publications:  Prof Dino Distefano

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. NASA FORMAL METHODS (NFM 2015). 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(2013). Runtime Verification Based on Register Automata. TACAS260-276-260-276.
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.
Rensink A, Distefano D(2006). Abstract Graph Transformation. Electron. Notes Theor. Comput. Sci. vol. 157, Article 1, 39-59.
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.
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.
Return to top