Moving Fast with Software Verification.

Cristiano Calcagno Cristiano Calcagno Dino Distefano Jérémy Dubreil Dominik Gabi Pieter Hooimeijer Martino Luca Peter W. O'Hearn Irene Papakonstantinou Jim Purbrick Dulma Rodriguez Moving Fast with Software Verification. 3-11 2015 NFM https://doi.org/10.1007/978-3-319-17524-9_1 https://www.wikidata.org/entity/Q59410749 conf/nfm/2015 db/conf/nfm/nfm2015.html#CalcagnoDDGHLOP15 Martin Nordio Cristiano Calcagno Carlo Alberto Furia Javanni: A Verifier for JavaScript. 231-234 2013 FASE https://doi.org/10.1007/978-3-642-37057-1_17 conf/fase/2013 db/conf/fase/fase2013.html#NordioCF13 Martin Nordio Cristiano Calcagno Bertrand Meyer 0001 Certificates and Separation Logic. 273-293 2013 TGC https://doi.org/10.1007/978-3-319-05119-2_16 conf/tgc/2013 db/conf/tgc/tgc2013.html#NordioCM13 Stephan van Staden Cristiano Calcagno Bertrand Meyer 0001 Freefinement. 7-18 2012 POPL https://doi.org/10.1145/2103656.2103661 https://doi.org/10.1145/2103621.2103661 conf/popl/2012 db/conf/popl/popl2012.html#StadenCM12

Josh Berdine Cristiano Calcagno Peter W. O'Hearn Verification Condition Generation and Variable Conditions in Smallfoot http://arxiv.org/abs/1204.4804 2012 CoRR abs/1204.4804 db/journals/corr/corr1204.html#abs-1204-4804

Cristiano Calcagno Dino Distefano Peter W. O'Hearn Hongseok Yang Compositional Shape Analysis by Means of Bi-Abduction. 26:1-26:66 2011 58 J. ACM 6 https://doi.org/10.1145/2049697.2049700 https://www.wikidata.org/entity/Q59410746 db/journals/jacm/jacm58.html#CalcagnoDOY11

Cristiano Calcagno Dino Distefano Infer: An Automatic Program Verifier for Memory Safety of C Programs. 459-465 2011 NASA Formal Methods https://doi.org/10.1007/978-3-642-20398-5_33 https://www.wikidata.org/entity/Q59410747 conf/nfm/2011 db/conf/nfm/nfm2011.html#CalcagnoD11

James Brotherston Cristiano Calcagno Classical BI: Its Semantics and Proof Theory http://arxiv.org/abs/1005.2340 2010 Log. Methods Comput. Sci. 6 db/journals/lmcs/lmcs6.html#abs-1005-2340 3

Cristiano Calcagno Thomas Dinsdale-Young Philippa Gardner Adjunct elimination in Context Logic for trees. 474-499 2010 208 Inf. Comput. 5 https://doi.org/10.1016/j.ic.2009.02.013 db/journals/iandc/iandc208.html#CalcagnoDG10

Stephan van Staden Cristiano Calcagno Bertrand Meyer 0001 Verifying Executable Object-Oriented Specifications with Separation Logic. 151-174 2010 ECOOP https://doi.org/10.1007/978-3-642-14107-2_8 conf/ecoop/2010 db/conf/ecoop/ecoop2010.html#StadenCM10 Stephan van Staden Cristiano Calcagno Reasoning about multiple related abstractions with MultiStar. 504-519 2010 OOPSLA https://doi.org/10.1145/1869459.1869501 https://doi.org/10.1145/1932682.1869501 conf/oopsla/2010 db/conf/oopsla/oopsla2010.html#StadenC10 Jules Villard Étienne Lozes Cristiano Calcagno Tracking Heaps That Hop with Heap-Hop. 275-279 2010 TACAS https://doi.org/10.1007/978-3-642-12002-2_23 conf/tacas/2010 db/conf/tacas/tacas2010.html#VillardLC10 Martin Nordio Cristiano Calcagno Bertrand Meyer 0001 Peter Müller 0001 Julian Tschannen Reasoning about Function Objects. 79-96 2010 TOOLS (48) https://doi.org/10.1007/978-3-642-13953-6_5 conf/tools/48-2010 db/conf/tools/tools48-2010.html#NordioCMMT10 Jules Villard Étienne Lozes Cristiano Calcagno Proving Copyless Message Passing. 194-209 2009 APLAS https://doi.org/10.1007/978-3-642-10672-9_15 conf/aplas/2009 db/conf/aplas/aplas2009.html#VillardLC09 Cristiano Calcagno Dino Distefano Viktor Vafeiadis Bi-abductive Resource Invariant Synthesis. 259-274 2009 APLAS https://doi.org/10.1007/978-3-642-10672-9_19 conf/aplas/2009 db/conf/aplas/aplas2009.html#CalcagnoDV09 Mohammad Raza Cristiano Calcagno Philippa Gardner Automatic Parallelization with Separation Logic. 348-362 2009 ESOP https://doi.org/10.1007/978-3-642-00590-9_25 conf/esop/2009 db/conf/esop/esop2009.html#RazaCG09 Cristiano Calcagno Dino Distefano Peter W. O'Hearn Hongseok Yang Compositional shape analysis by means of bi-abduction. 289-300 2009 POPL https://doi.org/10.1145/1480881.1480917 https://doi.org/10.1145/1594834.1480917 conf/popl/2009 db/conf/popl/popl2009.html#CalcagnoDOY09 James Brotherston Cristiano Calcagno Classical BI: a logic for reasoning about dualising resources. 328-339 2009 POPL https://doi.org/10.1145/1480881.1480923 https://doi.org/10.1145/1594834.1480923 conf/popl/2009 db/conf/popl/popl2009.html#BrotherstonC09 Martin Nordio Cristiano Calcagno Peter Müller 0001 Bertrand Meyer 0001 A Sound and Complete Program Logic for Eiffel. 195-214 2009 TOOLS (47) https://doi.org/10.1007/978-3-642-02571-6_12 conf/tools/47-2009 db/conf/tools/tools47-2009.html#NordioCMM09 Hongseok Yang Oukseh Lee Josh Berdine Cristiano Calcagno Byron Cook Dino Distefano Peter W. O'Hearn Scalable Shape Analysis for Systems Code. 385-398 2008 CAV https://doi.org/10.1007/978-3-540-70545-1_36 conf/cav/2008 db/conf/cav/cav2008.html#YangLBCCDO08 Cristiano Calcagno Dino Distefano Peter W. O'Hearn Hongseok Yang Space Invading Systems Code. 1-3 2008 LOPSTR https://doi.org/10.1007/978-3-642-00515-2_1 conf/lopstr/2008 db/conf/lopstr/lopstr2008.html#CalcagnoDOY08 James Brotherston Richard Bornat Cristiano Calcagno Cyclic proofs of program termination in separation logic. 101-112 2008 conf/popl/2008 POPL https://doi.org/10.1145/1328438.1328453 https://doi.org/10.1145/1328897.1328453 https://www.wikidata.org/entity/Q54086356 db/conf/popl/popl2008.html#BrotherstonBC08 Cristiano Calcagno Thomas Dinsdale-Young Philippa Gardner Adjunct Elimination in Context Logic for Trees. 255-270 2007 conf/aplas/2007 APLAS https://doi.org/10.1007/978-3-540-76637-7_17 db/conf/aplas/aplas2007.html#CalcagnoDG07 Josh Berdine Cristiano Calcagno Byron Cook Dino Distefano Peter W. O'Hearn Thomas Wies Hongseok Yang Shape Analysis for Composite Data Structures. 178-192 2007 conf/cav/2007 CAV https://doi.org/10.1007/978-3-540-73368-3_22 db/conf/cav/cav2007.html#BerdineCCDOWY07 Cristiano Calcagno Peter W. O'Hearn Hongseok Yang Local Action and Abstract Separation Logic. 366-378 2007 conf/lics/2007 LICS https://doi.org/10.1109/LICS.2007.30 https://doi.ieeecomputersociety.org/10.1109/LICS.2007.30 https://www.wikidata.org/entity/Q56445147 db/conf/lics/lics2007.html#CalcagnoOY07 Cristiano Calcagno Philippa Gardner Uri Zarfaty Context logic as modal logic: completeness and parametric inexpressivity. 123-134 2007 conf/popl/2007 POPL https://doi.org/10.1145/1190216.1190236 https://doi.org/10.1145/1190215.1190236 https://www.wikidata.org/entity/Q130863296 db/conf/popl/popl2007.html#CalcagnoGZ07 Cristiano Calcagno Matthew J. Parkinson Viktor Vafeiadis Modular Safety Checking for Fine-Grained Concurrency. 233-248 2007 conf/sas/2007 SAS https://doi.org/10.1007/978-3-540-74061-2_15 db/conf/sas/sas2007.html#CalcagnoPV07 Cristiano Calcagno Dino Distefano Peter W. O'Hearn Hongseok Yang Footprint Analysis: A Shape Analysis That Discovers Preconditions. 402-418 2007 conf/sas/2007 SAS https://doi.org/10.1007/978-3-540-74061-2_25 db/conf/sas/sas2007.html#CalcagnoDOY07 Cristiano Calcagno Philippa Gardner Uri Zarfaty Local Reasoning about Data Update. 133-175 2007 conf/birthday/2007plotkin Computation, Meaning, and Logic https://doi.org/10.1016/j.entcs.2007.02.006 db/journals/entcs/entcs172.html#CalcagnoGZ07 Matthew J. Parkinson Richard Bornat Cristiano Calcagno Variables as Resource in Hoare Logics. 137-146 2006 conf/lics/2006 LICS https://doi.org/10.1109/LICS.2006.52 https://doi.ieeecomputersociety.org/10.1109/LICS.2006.52 db/conf/lics/lics2006.html#ParkinsonBC06 Ik-Soon Kim Kwangkeun Yi Cristiano Calcagno A polymorphic modal type system for lisp-like multi-staged languages. 257-268 2006 conf/popl/2006 POPL https://doi.org/10.1145/1111037.1111060 https://doi.org/10.1145/1111320.1111060 db/conf/popl/popl2006.html#KimYC06 Cristiano Calcagno Dino Distefano Peter W. O'Hearn Hongseok Yang Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. 182-203 2006 conf/sas/2006 SAS https://doi.org/10.1007/11823230_13 db/conf/sas/sas2006.html#CalcagnoDOY06

Cristiano Calcagno Luca Cardelli Andrew D. Gordon 0001 Deciding validity in a spatial logic for trees. 543-572 2005 15 J. Funct. Program. 4 https://doi.org/10.1017/S0956796804005404 https://www.wikidata.org/entity/Q56982073 db/journals/jfp/jfp15.html#CalcagnoCG05

Josh Berdine Cristiano Calcagno Peter W. O'Hearn Symbolic Execution with Separation Logic. 52-68 2005 conf/aplas/2005 APLAS https://doi.org/10.1007/11575467_5 db/conf/aplas/aplas2005.html#BerdineCO05 Josh Berdine Cristiano Calcagno Peter W. O'Hearn Smallfoot: Modular Automatic Assertion Checking with Separation Logic. 115-137 2005 conf/fmco/2005 FMCO https://doi.org/10.1007/11804192_6 db/conf/fmco/fmco2005.html#BerdineCO05 Cristiano Calcagno Philippa Gardner Matthew Hague From Separation Logic to First-Order Logic. 395-409 https://doi.org/10.1007/978-3-540-31982-5_25 2005 conf/fossacs/2005 FoSSaCS db/conf/fossacs/fossacs2005.html#CalcagnoGH05 Richard Bornat Cristiano Calcagno Peter W. O'Hearn Matthew J. Parkinson Permission accounting in separation logic. 259-270 2005 conf/popl/2005 POPL https://doi.org/10.1145/1040305.1040327 https://doi.org/10.1145/1047659.1040327 https://www.wikidata.org/entity/Q130884290 db/conf/popl/popl2005.html#BornatCOP05 Cristiano Calcagno Philippa Gardner Uri Zarfaty Context logic and tree update. 271-282 2005 conf/popl/2005 POPL https://doi.org/10.1145/1040305.1040328 https://doi.org/10.1145/1047659.1040328 db/conf/popl/popl2005.html#CalcagnoGZ05 Richard Bornat Cristiano Calcagno Hongseok Yang Variables as Resource in Separation Logic. 247-276 2005 conf/mfps/2005 MFPS https://doi.org/10.1016/j.entcs.2005.11.059 db/journals/entcs/entcs155.html#BornatCY06

Cristiano Calcagno Two-level languages for program optimization. 61-81 2004 315 Theor. Comput. Sci. 1 https://doi.org/10.1016/j.tcs.2003.11.013 db/journals/tcs/tcs315.html#Calcagno04

Cristiano Calcagno Eugenio Moggi Walid Taha ML-Like Inference for Classifiers. 79-93 https://doi.org/10.1007/978-3-540-24725-8_7 2004 conf/esop/2004 ESOP db/conf/esop/esop2004.html#CalcagnoMT04 Josh Berdine Cristiano Calcagno Peter W. O'Hearn A Decidable Fragment of Separation Logic. 97-109 https://doi.org/10.1007/978-3-540-30538-5_9 2004 conf/fsttcs/2004 FSTTCS db/conf/fsttcs/fsttcs2004.html#BerdineCO04

Cristiano Calcagno Eugenio Moggi Tim Sheard Closed types for a safe imperative MetaML. 545-571 2003 13 J. Funct. Program. 3 https://doi.org/10.1017/S0956796802004598 db/journals/jfp/jfp13.html#CalcagnoMS03

Cristiano Calcagno Peter W. O'Hearn Richard Bornat Program logic and equivalence in the presence of garbage collection. 557-581 2003 3 Theor. Comput. Sci. 298 https://doi.org/10.1016/S0304-3975(02)00868-X db/journals/tcs/tcs298.html#CalcagnoOB03

Cristiano Calcagno Walid Taha Liwen Huang Xavier Leroy Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. 57-76 https://doi.org/10.1007/978-3-540-39815-8_4 2003 conf/gpce/2003 GPCE db/conf/gpce/gpce2003.html#CalcagnoTHL03 Cristiano Calcagno Luca Cardelli Andrew D. Gordon 0001 Deciding validity in a spatial logic for trees. 62-73 2003 conf/tldi/2003 TLDI https://doi.org/10.1145/604174.604183 https://doi.org/10.1145/640136.604183 db/conf/tldi/tldi2003.html#CalcagnoCG03

Cristiano Calcagno Simon Helsen Peter Thiemann 0001 Syntactic Type Soundness Results for the Region Calculus. 199-221 2002 173 Inf. Comput. 2 https://doi.org/10.1006/inco.2001.3112 db/journals/iandc/iandc173.html#CalcagnoHT02

Cristiano Calcagno Hongseok Yang Peter W. O'Hearn Computability and Complexity Results for a Spatial Assertion Language for Data Structures. 289-300 2001 conf/aplas/2001 APLAS db/conf/aplas/aplas2001.html#CalcagnoYO01 Cristiano Calcagno Peter W. O'Hearn On Garbage and Program Logic. 137-151 2001 conf/fossacs/2001 FoSSaCS https://doi.org/10.1007/3-540-45315-6_9 db/conf/fossacs/fossacs2001.html#CalcagnoO01 Cristiano Calcagno Hongseok Yang Peter W. O'Hearn Computability and Complexity Results for a Spatial Assertion Language for Data Structures. 108-119 2001 conf/fsttcs/2001 FSTTCS https://doi.org/10.1007/3-540-45294-X_10 db/conf/fsttcs/fsttcs2001.html#CalcagnoYO01 Cristiano Calcagno Stratified operational semantics for safety and correctness of the region calculus. 155-165 2001 conf/popl/2001 POPL https://doi.org/10.1145/360204.360217 https://doi.org/10.1145/373243.360217 db/conf/popl/popl2001.html#Calcagno01 Cristiano Calcagno Eugenio Moggi Walid Taha Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming. 25-36 https://doi.org/10.1007/3-540-45022-X_4 2000 conf/icalp/2000 ICALP db/conf/icalp/icalp2000.html#CalcagnoMT00 Cristiano Calcagno Samin S. Ishtiaq Peter W. O'Hearn Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292. 190-201 2000 conf/ppdp/2000 PPDP https://doi.org/10.1145/351268.351291 db/conf/ppdp/ppdp2000.html#CalcagnoIO00 Cristiano Calcagno Eugenio Moggi Multi-Stage Imperative Languages: A Conservative Extension Result. 92-107 https://doi.org/10.1007/3-540-45350-4_9 2000 conf/saig/2000 SAIG db/conf/saig/saig2000.html#CalcagnoM00 Josh Berdine Richard Bornat James Brotherston Luca Cardelli Byron Cook Thomas Dinsdale-Young Dino Distefano Jérémy Dubreil Carlo A. FuriaCarlo Alberto Furia Dominik Gabi Philippa Gardner Andrew D. Gordon 0001 Matthew Hague Simon Helsen Pieter Hooimeijer Liwen Huang Samin S. Ishtiaq Ik-Soon Kim Oukseh Lee Xavier Leroy Étienne Lozes Martino Luca Bertrand Meyer 0001 Eugenio Moggi Peter Müller 0001 Martín NordioMartin Nordio Peter W. O'Hearn Irene Papakonstantinou Matthew J. Parkinson Jim Purbrick Mohammad Raza Dulma Rodriguez Tim Sheard Stephan van Staden Walid Taha Peter Thiemann 0001 Julian Tschannen Viktor Vafeiadis Jules Villard Thomas Wies Hongseok Yang Kwangkeun Yi Uri Zarfaty