@misc(CCI,
 title        = "Common {C}ompiler {I}nfrastructure",
 url          = "http://cciast.codeplex.com/",
)
@article(ahrendt2005key,
 author       = "Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert and Richard Bubel and Martin Giese and Reiner H{\"a}hnle and Wolfram Menzel and Wojciech Mostowski and Andreas Roth and Steffen Schlager",
 year         = "2005",
 title        = "The key tool",
 journal      = "Software \& Systems Modeling",
 volume       = "4",
 number       = "1",
 pages        = "32--54",
 doi          = "10.1007/s10270-004-0058-x",
)
@inproceedings(AlbertBGHR12,
 author       = "Elvira Albert and Richard Bubel and Samir Genaim and Reiner H{\"a}hnle and Guillermo Rom{\'a}n-D\'{\i }ez",
 year         = "2012",
 title        = "Verified Resource Guarantees for Heap Manipulating Programs",
 booktitle    = "FASE",
 pages        = "130--145",
 doi          = "10.1007/978-3-642-28872-2\_10",
)
@inproceedings(AlbertGG09,
 author       = "Elvira Albert and Samir Genaim and Miguel G{\'o}mez-Zamalloa",
 year         = "2009",
 title        = "Live heap space analysis for languages with garbage collection",
 booktitle    = "ISMM",
 pages        = "129--138",
 doi          = "10.1145/1542431.1542450",
)
@article(albert12scp,
 author       = "Elvira Albert and Samir Genaim and Miguel G{\'o}mez-Zamalloa",
 year         = "2013",
 title        = "Heap space analysis for garbage collected languages",
 journal      = "Sci. Comput. Program.",
 volume       = "78",
 number       = "9",
 pages        = "1427--1448",
 doi          = "10.1016/j.scico.2012.10.008",
)
@article(Atkey2011,
 author       = "Robert Atkey",
 year         = "2011",
 title        = "{Amortised Resource Analysis with Separation Logic}",
 journal      = "Logical Methods in Computer Science",
 volume       = "7",
 number       = "2",
 doi          = "10.2168/LMCS-7(2:17)2011",
)
@inproceedings(garber07iwaco,
 author       = "Michael Barnett and Manuel F{\"a}ndrich and Diego Garbervetsky and Francesco Logozzo",
 year         = "2007",
 title        = "Annotations for (more) Precise Points-to Analysis",
 booktitle    = "Proceedings of the 2nd International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'07)",
 pages        = "11--18",
 url          = "http://people.dsv.su.se/~tobias/iwaco/p4-barnett.pdf",
)
@inproceedings(BarthePS05,
 author       = "Gilles Barthe and Mariela Pavlova and Gerardo Schneider",
 year         = "2005",
 title        = "Precise Analysis of Memory Consumption using Program Logics.",
 booktitle    = "SEFM",
 pages        = "86--95",
 doi          = "10.1109/SEFM.2005.34",
)
@misc(z3,
 author       = "Nikolaj Bjorner and Leonardo de Moura",
 year         = "2009",
 title        = "Z3: An efficient SMT solver",
 howpublished = "http://research.microsoft.com/en-us/um/redmond/projects/z3/",
 doi          = "10.1007/978-3-540-78800-3\_24",
)
@inproceedings(garber08ismm,
 author       = "V{\'\i }ctor Braberman and Federico Fern{\'a}ndez and Diego Garbervetsky and Sergio Yovine",
 year         = "2008",
 title        = "Parametric prediction of heap memory requirements",
 booktitle    = "Proceedings of the 7th international symposium on Memory management",
 organization = "ACM",
 pages        = "141--150",
 doi          = "10.1145/1375634.1375655",
)
@article(garber12scp,
 author       = "V\'{\i }ctor A. Braberman and Diego Garbervetsky and Samuel Hym and Sergio Yovine",
 year         = "2013",
 title        = "Summary-based inference of quantitative bounds of live heap objects",
 journal      = "Submitted",
)
@inproceedings(chin05SAS,
 author       = "Wei-Ngan Chin and Huu Hai Nguyen and Shengchao Qin and Martin Rinard",
 year         = "2005",
 title        = "Memory Usage Verification for OO Programs",
 booktitle    = "SAS 05",
 doi          = "10.1007/11547662\_7",
)
@article(clauss2009symbolic,
 author       = "Philippe Clauss and Federico Javier Fern{\'a}ndez and Diego Garbervetsky and Sven Verdoolaege",
 year         = "2009",
 title        = "{Symbolic polynomial maximization over convex sets and its application to memory requirement estimation}",
 journal      = "TVLSI",
 volume       = "17",
 number       = "8",
 pages        = "983--996",
 doi          = "10.1109/TVLSI.2008.2002049",
)
@inproceedings(Cousot77,
 author       = "Patrick Cousot and Radhia Cousot",
 year         = "1977",
 title        = "Abstract Interpretation: {A} Unified Lattice Model for Static Analysis of Programs by Construction of Approximation of Fixed Points",
 booktitle    = "POPL 77",
 pages        = "238--252",
 doi          = "10.1145/512950.512973",
)
@conference(fahndrich2010embedded,
 author       = "Manuel F{\"a}hndrich and Michael Barnett and Francesco Logozzo",
 year         = "2010",
 title        = "{Embedded contract languages}",
 booktitle    = "SAC 2010",
 organization = "ACM",
 pages        = "2103--2110",
 doi          = "10.1145/1774088.1774531",
)
@misc(clousot,
 author       = "Manuel F{\"a}hndrich and Francesco Logozzo",
 year         = "2009",
 title        = "Clousot: a language agnostic abstract interpretation-based static analyzer for .NET",
 howpublished = "http://research.microsoft.com/en-us/people/logozzo/",
)
@article(garber11cpe,
 author       = "Diego Garbervetsky and Sergio Yovine and V\'{\i }ctor A. Braberman and Mart\'{\i }n Rouaux and Alejandro Taboada",
 year         = "2011",
 title        = "Quantitative dynamic-memory analysis for Java",
 journal      = "Concurrency and Computation: Practice and Experience",
 volume       = "23",
 number       = "14",
 pages        = "1665--1678",
 doi          = "10.1002/cpe.1656",
)
@book(bollella00realtime,
 author       = "James Gosling and Greg Bollella",
 year         = "2000",
 title        = "The Real-Time Specification for Java",
 publisher    = "Addison-Wesley Longman Publishing Co., Inc.",
)
@conference(gulwani2010reachability,
 author       = "Sumit Gulwani and Florian Zuleger",
 year         = "2010",
 title        = "{The reachability-bound problem}",
 booktitle    = "PLDI'10",
 organization = "ACM",
 pages        = "292--304",
 doi          = "10.1145/1809028.1806630",
)
@article(he2009memory,
 author       = "Guanhua He and Shengchao Qin and Chenguang Luo and Wei-Ngan Chin",
 title        = "{Memory Usage Verification Using Hip/Sleek}",
 journal      = "ATVA'09",
 pages        = "166--181",
 doi          = "10.1007/978-3-642-04761-9\_14",
)
@article(hoffmann2010amortized,
 author       = "Jan Hoffmann and Martin Hofmann",
 year         = "2010",
 title        = "{Amortized resource analysis with polynomial potential}",
 journal      = "Programming Languages and Systems",
 pages        = "287--306",
 doi          = "10.1007/978-3-642-11957-6\_16",
)
@inproceedings(hofm03,
 author       = "Martin Hofman and Stefen Jost",
 year         = "2003",
 title        = "Static Prediction of Heap Usage for First-Order Functional Programs",
 booktitle    = "POPL 03",
 series       = "SIGPLAN",
 address      = "New Orleans, LA",
 doi          = "10.1145/640128.604148",
)
@inproceedings(leavens00jml,
 author       = "Gary T. Leavens and K. Rustan M. Leino and Erik Poll and Clyde Ruby and Bart Jacobs",
 year         = "2000",
 title        = "{JML}: notations and tools supporting detailed design in {Java}",
 booktitle    = "{OOPSLA}'00",
 pages        = "105--106",
 doi          = "10.1145/367845.367996",
)
@book(Meyer:OOP,
 author       = "Bertrand Meyer",
 year         = "1988",
 title        = "Object-oriented Software Construction",
 series       = "Series in Computer Science",
 publisher    = "Prentice-Hall International",
 address      = "New York",
)
@book(Meyer:Eiffel,
 author       = "Bertrand Meyer",
 year         = "1992",
 title        = "Eiffel: The Language",
 publisher    = "Prentice Hall",
 address      = "Hemel Hempstead",
)