Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming. - Cristiano Calcagno; Eugenio Moggi; Walid Taha (ICALP, 2000)

Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292. - Cristiano Calcagno; Samin S. Ishtiaq; Peter W. O'Hearn (PPDP, 2000)

Multi-Stage Imperative Languages: A Conservative Extension Result. - Cristiano Calcagno; Eugenio Moggi (SAIG, 2000)

Computability and Complexity Results for a Spatial Assertion Language for Data Structures. - Cristiano Calcagno; Hongseok Yang; Peter W. O'Hearn (APLAS, 2001)

On Garbage and Program Logic. - Cristiano Calcagno; Peter W. O'Hearn (FoSSaCS, 2001)

Stratified operational semantics for safety and correctness of the region calculus. - Cristiano Calcagno (POPL, 2001)

Syntactic Type Soundness Results for the Region Calculus. - Cristiano Calcagno; Simon Helsen; Peter Thiemann 001 (Inf. Comput., 2002)

Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. - Cristiano Calcagno; Walid Taha; Liwen Huang; Xavier Leroy (GPCE, 2003)

Closed types for a safe imperative MetaML. - Cristiano Calcagno; Eugenio Moggi; Tim Sheard (J. Funct. Program., 2003)

Program logic and equivalence in the presence of garbage collection. - Cristiano Calcagno; Peter W. O'Hearn; Richard Bornat (Theor. Comput. Sci., 2003)

ML-Like Inference for Classifiers. - Cristiano Calcagno; Eugenio Moggi; Walid Taha (ESOP, 2004)

A Decidable Fragment of Separation Logic. - Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn (FSTTCS, 2004)

Two-level languages for program optimization. - Cristiano Calcagno (Theor. Comput. Sci., 2004)

Symbolic Execution with Separation Logic. - Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn (APLAS, 2005)

Smallfoot: Modular Automatic Assertion Checking with Separation Logic. - Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn (FMCO, 2005)

From Separation Logic to First-Order Logic. - Cristiano Calcagno; Philippa Gardner; Matthew Hague (FoSSaCS, 2005)

Permission accounting in separation logic. - Richard Bornat; Cristiano Calcagno; Peter W. O'Hearn; Matthew J. Parkinson (POPL, 2005)

Context logic and tree update. - Cristiano Calcagno; Philippa Gardner; Uri Zarfaty (POPL, 2005)

Variables as Resource in Separation Logic. - Richard Bornat; Cristiano Calcagno; Hongseok Yang (MFPS, 2005)

Deciding validity in a spatial logic for trees. - Cristiano Calcagno; Luca Cardelli; Andrew D. Gordon 001 (J. Funct. Program., 2005)

Variables as Resource in Hoare Logics. - Matthew J. Parkinson; Richard Bornat; Cristiano Calcagno (LICS, 2006)

A polymorphic modal type system for lisp-like multi-staged languages. - Ik-Soon Kim; Kwangkeun Yi; Cristiano Calcagno (POPL, 2006)

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. - Cristiano Calcagno; Dino Distefano; Peter W. O'Hearn; Hongseok Yang (SAS, 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)

Local Action and Abstract Separation Logic. - Cristiano Calcagno; Peter W. O'Hearn; Hongseok Yang (LICS, 2007)

Context logic as modal logic: completeness and parametric inexpressivity. - Cristiano Calcagno; Philippa Gardner; Uri Zarfaty (POPL, 2007)

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

Modular Safety Checking for Fine-Grained Concurrency. - Cristiano Calcagno; Matthew J. Parkinson; Viktor Vafeiadis (SAS, 2007)

Local Reasoning about Data Update. - Cristiano Calcagno; Philippa Gardner; Uri Zarfaty (Computation, Meaning, and Logic, 2007)

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)

Cyclic proofs of program termination in separation logic. - James Brotherston; Richard Bornat; Cristiano Calcagno (POPL, 2008)

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

Proving Copyless Message Passing. - Jules Villard; Étienne Lozes; Cristiano Calcagno (APLAS, 2009)

Automatic Parallelization with Separation Logic. - Mohammad Raza; Cristiano Calcagno; Philippa Gardner (ESOP, 2009)

Classical BI: a logic for reasoning about dualising resources. - James Brotherston; Cristiano Calcagno (POPL, 2009)

A Sound and Complete Program Logic for Eiffel. - Martin Nordio; Cristiano Calcagno; Peter Müller 001; Bertrand Meyer 001 (TOOLS (47), 2009)

Verifying Executable Object-Oriented Specifications with Separation Logic. - Stephan van Staden; Cristiano Calcagno; Bertrand Meyer 001 (ECOOP, 2010)

Reasoning about multiple related abstractions with MultiStar. - Stephan van Staden; Cristiano Calcagno (OOPSLA, 2010)

Tracking Heaps That Hop with Heap-Hop. - Jules Villard; Étienne Lozes; Cristiano Calcagno (TACAS, 2010)

Reasoning about Function Objects. - Martin Nordio; Cristiano Calcagno; Bertrand Meyer 001; Peter Müller 001; Julian Tschannen (TOOLS (48), 2010)

Classical BI: Its Semantics and Proof Theory - James Brotherston; Cristiano Calcagno (Log. Methods Comput. Sci., 2010)

Adjunct elimination in Context Logic for trees. - Cristiano Calcagno; Thomas Dinsdale-Young; Philippa Gardner (Inf. Comput., 2010)

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

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

Freefinement. - Stephan van Staden; Cristiano Calcagno; Bertrand Meyer 001 (POPL, 2012)

Verification Condition Generation and Variable Conditions in Smallfoot - Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn (CoRR, 2012)

Javanni: A Verifier for JavaScript. - Martin Nordio; Cristiano Calcagno; Carlo Alberto Furia (FASE, 2013)

Certificates and Separation Logic. - Martin Nordio; Cristiano Calcagno; Bertrand Meyer 001 (TGC, 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)