Travelled to:
1 × Canada
1 × Cyprus
1 × Denmark
1 × France
1 × Korea
1 × Poland
1 × Slovenia
2 × Germany
2 × Italy
2 × Switzerland
3 × Spain
3 × United Kingdom
8 × USA
Collaborated with:
P.W.O'Hearn H.Yang P.Gardner D.Distefano S.v.Staden E.Moggi B.Meyer R.Bornat M.J.Parkinson W.Taha J.Brotherston M.Nordio U.Zarfaty ∅ P.Müller C.A.Furia J.Villard É.Lozes M.Raza V.Vafeiadis I.Kim K.Yi M.Hague S.S.Ishtiaq J.Berdine B.Cook L.Huang X.Leroy J.Tschannen O.Lee T.Wies
Talks about:
logic (15) analysi (6) separ (6) shape (5) multi (5) program (4) stage (4) abstract (3) languag (3) system (3)
Person: Cristiano Calcagno
DBLP: Calcagno:Cristiano
Contributed to:
Wrote 31 papers:
- FASE-2013-NordioCF #javascript #named #verification
- Javanni: A Verifier for JavaScript (MN, CC, CAF), pp. 231–234.
- POPL-2012-StadenCM
- Freefinement (SvS, CC, BM), pp. 7–18.
- ECOOP-2010-StadenCM #execution #logic #object-oriented #specification #verification
- Verifying Executable Object-Oriented Specifications with Separation Logic (SvS, CC, BM), pp. 151–174.
- OOPSLA-2010-StadenC #abstraction #multi #reasoning
- Reasoning about multiple related abstractions with MultiStar (SvS, CC), pp. 504–519.
- TACAS-2010-VillardLC
- Tracking Heaps That Hop with Heap-Hop (JV, ÉL, CC), pp. 275–279.
- TOOLS-EUROPE-2010-NordioCMMT #reasoning
- Reasoning about Function Objects (MN, CC, BM, PM, JT), pp. 79–96.
- ESOP-2009-RazaCG #automation #logic #parallel
- Automatic Parallelization with Separation Logic (MR, CC, PG), pp. 348–362.
- POPL-2009-BrotherstonC #logic #reasoning
- Classical BI: a logic for reasoning about dualising resources (JB, CC), pp. 328–339.
- POPL-2009-CalcagnoDOY #analysis #composition
- Compositional shape analysis by means of bi-abduction (CC, DD, PWO, HY), pp. 289–300.
- TOOLS-EUROPE-2009-NordioCMM #eiffel #logic
- A Sound and Complete Program Logic for Eiffel (MN, CC, PM, BM), pp. 195–214.
- CAV-2008-YangLBCCDO #analysis #scalability
- Scalable Shape Analysis for Systems Code (HY, OL, JB, CC, BC, DD, PWO), pp. 385–398.
- LOPSTR-2008-CalcagnoDOY
- Space Invading Systems Code (CC, DD, PWO, HY), pp. 1–3.
- POPL-2008-BrotherstonBC #logic #proving #termination
- Cyclic proofs of program termination in separation logic (JB, RB, CC), pp. 101–112.
- CAV-2007-BerdineCCDOWY #analysis #data type
- Shape Analysis for Composite Data Structures (JB, CC, BC, DD, PWO, TW, HY), pp. 178–192.
- LICS-2007-CalcagnoOY #logic
- Local Action and Abstract Separation Logic (CC, PWO, HY), pp. 366–378.
- POPL-2007-CalcagnoGZ #logic #parametricity
- Context logic as modal logic: completeness and parametric inexpressivity (CC, PG, UZ), pp. 123–134.
- SAS-2007-CalcagnoDOY #analysis
- Footprint Analysis: A Shape Analysis That Discovers Preconditions (CC, DD, PWO, HY), pp. 402–418.
- SAS-2007-CalcagnoPV #composition #concurrent #fine-grained #safety
- Modular Safety Checking for Fine-Grained Concurrency (CC, MJP, VV), pp. 233–248.
- LICS-2006-ParkinsonBC #hoare #logic
- Variables as Resource in Hoare Logics (MJP, RB, CC), pp. 137–146.
- POPL-2006-KimYC #multi #polymorphism #type system
- A polymorphic modal type system for lisp-like multi-staged languages (ISK, KY, CC), pp. 257–268.
- SAS-2006-CalcagnoDOY #abstraction #pointer #reachability
- Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic (CC, DD, PWO, HY), pp. 182–203.
- FoSSaCS-2005-CalcagnoGH #first-order #logic
- From Separation Logic to First-Order Logic (CC, PG, MH), pp. 395–409.
- POPL-2005-BornatCOP #logic
- Permission accounting in separation logic (RB, CC, PWO, MJP), pp. 259–270.
- POPL-2005-CalcagnoGZ #logic
- Context logic and tree update (CC, PG, UZ), pp. 271–282.
- ESOP-2004-CalcagnoMT #classification
- ML-Like Inference for Classifiers (CC, EM, WT), pp. 79–93.
- GPCE-2003-CalcagnoTHL #abstract syntax tree #implementation #multi #using
- Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection (CC, WT, LH, XL), pp. 57–76.
- FoSSaCS-2001-CalcagnoO #logic #on the
- On Garbage and Program Logic (CC, PWO), pp. 137–151.
- POPL-2001-Calcagno #calculus #correctness #safety #semantics
- Stratified operational semantics for safety and correctness of the region calculus (CC), pp. 155–165.
- ICALP-2000-CalcagnoMT #approach #imperative #multi #programming
- Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming (CC, EM, WT), pp. 25–36.
- PPDP-2000-CalcagnoIO #alias #analysis #hoare #logic #pointer #semantics
- Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292 (CC, SSI, PWO), pp. 190–201.
- SAIG-2000-CalcagnoM #imperative #multi
- Multi-Stage Imperative Languages: A Conservative Extension Result (CC, EM), pp. 92–107.