Cristiano Calcagno

54 papers A* 14A 5B 13C 2Journal 9Unranked 11
YearRankTypeTitle / Venue / Authors
2015 — conf
Moving Fast with Software Verification.
NFM
Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Rodriguez
2013 — conf
Certificates and Separation Logic.
TGC
Martin Nordio, Cristiano Calcagno, Bertrand Meyer
2013 B conf
Javanni: A Verifier for JavaScript.
FASE
Martin Nordio, Cristiano Calcagno, Carlo Alberto Furia
2012 A* conf
Freefinement.
POPL
Stephan van Staden, Cristiano Calcagno, Bertrand Meyer
2012 J jnl
Verification Condition Generation and Variable Conditions in Smallfoot
CoRR
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2011 J jnl
Compositional Shape Analysis by Means of Bi-Abduction.
J. ACM
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2011 — conf
Infer: An Automatic Program Verifier for Memory Safety of C Programs.
NASA Formal Methods
Cristiano Calcagno, Dino Distefano
2010 J jnl
Adjunct elimination in Context Logic for trees.
Inf. Comput.
Cristiano Calcagno, Thomas Dinsdale-Young, Philippa Gardner
2010 J jnl
Classical BI: Its Semantics and Proof Theory
Log. Methods Comput. Sci.
James Brotherston, Cristiano Calcagno
2010 — conf
Reasoning about Function Objects.
TOOLS (48)
Martin Nordio, Cristiano Calcagno, Bertrand Meyer, Peter Müller, Julian Tschannen
2010 A conf
Reasoning about multiple related abstractions with MultiStar.
OOPSLA
Stephan van Staden, Cristiano Calcagno
2010 A conf
Tracking Heaps That Hop with Heap-Hop.
TACAS
Jules Villard, Étienne Lozes, Cristiano Calcagno
2010 A conf
Verifying Executable Object-Oriented Specifications with Separation Logic.
ECOOP
Stephan van Staden, Cristiano Calcagno, Bertrand Meyer
2009 — conf
A Sound and Complete Program Logic for Eiffel.
TOOLS (47)
Martin Nordio, Cristiano Calcagno, Peter Müller, Bertrand Meyer
2009 A conf
Automatic Parallelization with Separation Logic.
ESOP
Mohammad Raza, Cristiano Calcagno, Philippa Gardner
2009 B conf
Bi-abductive Resource Invariant Synthesis.
APLAS
Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis
2009 A* conf
Classical BI: a logic for reasoning about dualising resources.
POPL
James Brotherston, Cristiano Calcagno
2009 A* conf
Compositional shape analysis by means of bi-abduction.
POPL
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2009 B conf
Proving Copyless Message Passing.
APLAS
Jules Villard, Étienne Lozes, Cristiano Calcagno
2008 A* conf
Cyclic proofs of program termination in separation logic.
POPL
James Brotherston, Richard Bornat, Cristiano Calcagno
2008 A* conf
Scalable Shape Analysis for Systems Code.
CAV
Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn
2008 C conf
Space Invading Systems Code.
LOPSTR
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2007 B conf
Adjunct Elimination in Context Logic for Trees.
APLAS
Cristiano Calcagno, Thomas Dinsdale-Young, Philippa Gardner
2007 A* conf
Context logic as modal logic: completeness and parametric inexpressivity.
POPL
Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
2007 B conf
Footprint Analysis: A Shape Analysis That Discovers Preconditions.
SAS
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2007 A* conf
Local Action and Abstract Separation Logic.
LICS
Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang
2007 — conf
Local Reasoning about Data Update.
Computation, Meaning, and Logic
Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
2007 B conf
Modular Safety Checking for Fine-Grained Concurrency.
SAS
Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis
2007 A* conf
Shape Analysis for Composite Data Structures.
CAV
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang
2006 A* conf
A polymorphic modal type system for lisp-like multi-staged languages.
POPL
Ik-Soon Kim, Kwangkeun Yi, Cristiano Calcagno
2006 B conf
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic.
SAS
Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang
2006 A* conf
Variables as Resource in Hoare Logics.
LICS
Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno
2005 A* conf
Context logic and tree update.
POPL
Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
2005 J jnl
Deciding validity in a spatial logic for trees.
J. Funct. Program.
Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon
2005 B conf
From Separation Logic to First-Order Logic.
FoSSaCS
Cristiano Calcagno, Philippa Gardner, Matthew Hague
2005 A* conf
Permission accounting in separation logic.
POPL
Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson
2005 — conf
Smallfoot: Modular Automatic Assertion Checking with Separation Logic.
FMCO
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2005 B conf
Symbolic Execution with Separation Logic.
APLAS
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2005 B conf
Variables as Resource in Separation Logic.
MFPS
Richard Bornat, Cristiano Calcagno, Hongseok Yang
2004 — conf
A Decidable Fragment of Separation Logic.
FSTTCS
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
2004 A conf
ML-Like Inference for Classifiers.
ESOP
Cristiano Calcagno, Eugenio Moggi, Walid Taha
2004 J jnl
Two-level languages for program optimization.
Theor. Comput. Sci.
Cristiano Calcagno
2003 J jnl
Closed types for a safe imperative MetaML.
J. Funct. Program.
Cristiano Calcagno, Eugenio Moggi, Tim Sheard
2003 — conf
Deciding validity in a spatial logic for trees.
TLDI
Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon
2003 B conf
Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection.
GPCE
Cristiano Calcagno, Walid Taha, Liwen Huang, Xavier Leroy
2003 J jnl
Program logic and equivalence in the presence of garbage collection.
Theor. Comput. Sci.
Cristiano Calcagno, Peter W. O'Hearn, Richard Bornat
2002 J jnl
Syntactic Type Soundness Results for the Region Calculus.
Inf. Comput.
Cristiano Calcagno, Simon Helsen, Peter Thiemann
2001 B conf
Computability and Complexity Results for a Spatial Assertion Language for Data Structures.
APLAS
Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn
2001 — conf
Computability and Complexity Results for a Spatial Assertion Language for Data Structures.
FSTTCS
Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn
2001 B conf
On Garbage and Program Logic.
FoSSaCS
Cristiano Calcagno, Peter W. O'Hearn
2001 A* conf
Stratified operational semantics for safety and correctness of the region calculus.
POPL
Cristiano Calcagno
2000 A* conf
Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming.
ICALP
Cristiano Calcagno, Eugenio Moggi, Walid Taha
2000 — conf
Multi-Stage Imperative Languages: A Conservative Extension Result.
SAIG
Cristiano Calcagno, Eugenio Moggi
2000 C conf
Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292.
PPDP
Cristiano Calcagno, Samin S. Ishtiaq, Peter W. O'Hearn