Research menu
Jump to menu

Publications:  Dr Dino Distefano

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 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,
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 et al. (2012) . Verification of Snapshot Isolation in Transactional Memory Java Programs. ECOOP. 640-664-640-664.
Calcagno C, Distefano D, O'Hearn PW et al. (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 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 et al. (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 et al. (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 et al. (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 et al. (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 et al. (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 et al. (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 et al. (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 et al. (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.Electr. Notes Theor. Comput. Sci. vol. 157, Article 1, 39-59.
Berdine J, Cook B, Distefano D et al. (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 et al. (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.
Grigore R, Distefano D, Petersen RL et al.. Runtime Verification Based on Register Automata.
Return to top