References

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

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org