On a Temporal Logic for Object-Based Systems. - Dino Distefano; Joost-Pieter Katoen; Arend Rensink (FMOODS, 2000)

Model Checking Birth and Death. - Dino Distefano; Arend Rensink; Joost-Pieter Katoen (IFIP TCS, 2002)

Who is Pointing When to Whom? - Dino Distefano; Joost-Pieter Katoen; Arend Rensink (FSTTCS, 2004)

A Parametric Model for the Analysis of Mobile Ambients. - Dino Distefano (APLAS, 2005)

Safety and Liveness in Concurrent Pointer Programs. - Dino Distefano; Joost-Pieter Katoen; Arend Rensink (FMCO, 2005)

Abstract Graph Transformation. - Arend Rensink; Dino Distefano (SVV@ICFEM, 2005)

Automatic Termination Proofs for Programs with Shape-Shifting Heaps. - Josh Berdine; Byron Cook; Dino Distefano; Peter W. O'Hearn (CAV, 2006)

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. - Cristiano Calcagno; Dino Distefano; Peter W. O'Hearn; Hongseok Yang (SAS, 2006)

A Local Shape Analysis Based on Separation Logic. - Dino Distefano; Peter W. O'Hearn; Hongseok Yang (TACAS, 2006)

Shape Analysis for Composite Data Structures. - Josh Berdine; Cristiano Calcagno; Byron Cook; Dino Distefano; Peter W. O'Hearn; Thomas Wies; Hongseok Yang (CAV, 2007)

Variance analyses from invariance analyses. - Josh Berdine; Aziem Chawdhary; Byron Cook; Dino Distefano; Peter W. O'Hearn (POPL, 2007)

Footprint Analysis: A Shape Analysis That Discovers Preconditions. - Cristiano Calcagno; Dino Distefano; Peter W. O'Hearn; Hongseok Yang (SAS, 2007)

Abductive Inference for Reasoning about Heaps. - Dino Distefano (APLAS, 2008)

Scalable Shape Analysis for Systems Code. - Hongseok Yang; Oukseh Lee; Josh Berdine; Cristiano Calcagno; Byron Cook; Dino Distefano; Peter W. O'Hearn (CAV, 2008)

Space Invading Systems Code. - Cristiano Calcagno; Dino Distefano; Peter W. O'Hearn; Hongseok Yang (LOPSTR, 2008)

jStar: towards practical verification for java. - Dino Distefano; Matthew J. Parkinson (OOPSLA, 2008)

Bi-abductive Resource Invariant Synthesis. - Cristiano Calcagno; Dino Distefano; Viktor Vafeiadis (APLAS, 2009)

Attacking Large Industrial Code with Bi-abductive Inference. - Dino Distefano (FMICS, 2009)

Memory Leaks Detection in Java by Bi-abductive Inference. - Dino Distefano; Ivana Filipovic (FASE, 2010)

Automated Cyclic Entailment Proofs in Separation Logic. - James Brotherston; Dino Distefano; Rasmus Lerchedahl Petersen (CADE, 2011)

The COST IC0701 Verification Competition 2011. - Thorsten Bormer; Marc Brockschmidt; Dino Distefano; Gidon Ernst; Jean-Christophe Filliâtre; Radu Grigore; Marieke Huisman; Vladimir Klebanov; Claude Marché; Rosemary Monahan; Wojciech Mostowski; Nadia Polikarpova; et al. (FoVeOOS, 2011)

Infer: An Automatic Program Verifier for Memory Safety of C Programs. - Cristiano Calcagno; Dino Distefano (NASA Formal Methods, 2011)

jStar-eclipse: an IDE for automated verification of Java programs. - Daiva Naudziuniene; Matko Botincan; Dino Distefano; Mike Dodds; Radu Grigore; Matthew J. Parkinson (SIGSOFT FSE, 2011)

Compositional Shape Analysis by Means of Bi-Abduction. - Cristiano Calcagno; Dino Distefano; Peter W. O'Hearn; Hongseok Yang (J. ACM, 2011)

Verification of Snapshot Isolation in Transactional Memory Java Programs. - Ricardo J. Dias; Dino Distefano; João Costa Seco; João Lourenço (ECOOP, 2012)

A Voyage to the Deep-Heap. - Dino Distefano (SAS, 2012)

Runtime Verification Based on Register Automata. - Radu Grigore; Dino Distefano; Rasmus Lerchedahl Petersen; Nikos Tzevelekos (TACAS, 2013)

Detecting Data Races on OpenCL Kernels with Symbolic Execution. - Dino Distefano; Jérémy Dubreil (CoRR, 2013)

Moving Fast with Software Verification. - Cristiano Calcagno; Dino Distefano; Jérémy Dubreil; Dominik Gabi; Pieter Hooimeijer; Martino Luca; Peter W. O'Hearn; Irene Papakonstantinou; Jim Purbrick; Dulma Rodriguez (NFM, 2015)

Information Leakage Analysis of Complex C Code and Its application to OpenSSL. - Pasquale Malacaria; Michael Tautschnig; Dino Distefano (ISoLA (1), 2016)

Scaling static analyses at Facebook. - Dino Distefano; Manuel Fähndrich; Francesco Logozzo; Peter W. O'Hearn (Commun. ACM, 2019)

Static Resource Analysis at Scale (Extended Abstract). - Ezgi Çiçek; Mehdi Bouaziz; Sungkeun Cho; Dino Distefano (SAS, 2020)

InfERL: scalable and extensible Erlang static analysis. - Ákos Hajdu; Matteo Marescotti; Thibault Suzanne; Ke Mao; Radu Grigore; Per Gustafsson; Dino Distefano (Erlang Workshop, 2022)

FAUSTA: Scaling Dynamic Analysis with Traffic Generation at WhatsApp. - Ke Mao; Timotej Kapus; Lambros Petrou; Ákos Hajdu; Matteo Marescotti; Andreas Löscher; Mark Harman; Dino Distefano (ICST, 2022)

Automatic Compositional Checking of Multi-object TypeState Properties of Software. - Radu Grigore; Dino Distefano; Nikos Tzevelekos (Principles of Verification (1), 2024)

PrivacyCAT: Privacy-Aware Code Analysis at Scale. - Ke Mao; Cons Åhs; Sopot Cela; Dino Distefano; Nick Gardner; Radu Grigore; Per Gustafsson; Ákos Hajdu; Timotej Kapus; Matteo Marescotti; Gabriela Cunha Sampaio; Thibault Suzanne (ICSE-SEIP, 2024)

Enhancing Compositional Static Analysis with Dynamic Analysis. - Dino Distefano; Matteo Marescotti; Cons Åhs; Sopot Cela; Gabriela Cunha Sampaio; Radu Grigore; Ákos Hajdu; Timotej Kapus; Ke Mao; Thibault Suzanne (ASE, 2024)