Menu
 
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,
10.1007/978-3-319-47166-2_63
http://qmro.qmul.ac.uk/xmlui/handle/123456789/13880
Calcagno C, Distefano D, Dubreil J et al. (2015) . Moving Fast with Software Verification. NASA FORMAL METHODS (NFM 2015). vol. 9058, 3-11.
10.1007/978-3-319-17524-9_1
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.
10.1007/978-3-642-33125-1_2
Dias RJ, Distefano D, Seco JAC et al. (2012) . Verification of Snapshot Isolation in Transactional Memory Java Programs. ECOOP. 640-664-640-664.
10.1007/978-3-642-31057-7_28
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,
10.1145/2049697.2049700
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.
10.1007/978-3-642-22438-6_12
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.
10.1007/978-3-642-31762-0_2
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.
10.1145/2025113.2025182
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.
10.1007/978-3-642-12029-9_20
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,
10.1007/978-3-642-04570-7_1
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},
10.1007/978-3-642-10672-9_19
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.
10.1145/1480881.1480917
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.
10.1007/978-3-642-00515-2_1
Distefano D (2008) . Abductive Inference for Reasoning about Heaps. PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS. Editors: Ramalingam, G, vol. 5356, 1-2.
10.1007/978-3-540-89330-1_1
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.
10.1007/978-3-540-70545-1_36
Distefano D, Parkinson MJ (2008) . jStar: Towards Practical Verification for Java. OOPSLA 2008 NASHVILLE, CONFERENCE PROCEEDINGS. 213-226.
10.1145/1449764.1449782
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.
10.1007/978-3-540-74061-2_25
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.
10.1007/978-3-540-73368-3_22
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.
10.1145/1190216.1190249
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.
10.1007/11691372_19
Rensink A, Distefano D (2006) . Abstract Graph Transformation.Electr. Notes Theor. Comput. Sci. vol. 157, Article 1, 39-59.
10.1016/j.entcs.2006.01.022
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.
10.1007/11817963_35
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.
10.1007/11823230_13
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.
10.1007/11804192_14
Distefano D (2005) . A parametric model for the analysis of mobile ambients. PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS. Editors: Yi, K, vol. 3780, 401-417.
10.1007/11575467_26
Distefano D, Katoen J-P, Rensink A (2004) . Who is Pointing When to Whom?. FSTTCS. Editors: Lodaya, K, Mahajan, M, vol. 3328, 250-262.
10.1007/978-3-540-30538-5_21
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.
10.1007/978-3-642-36742-7_19
http://qmro.qmul.ac.uk/xmlui/handle/123456789/19031
Return to top