Abstract:
In this paper we present an approach to check resource consumption contracts using an off-theshelf static analyzer. We propose a set of annotations to support resource usage specifications, in particular, dynamic memory consumption constraints. Since dynamic memory may be recycled by a memory manager, the consumption of this resource is not monotone. The specification language can express both memory consumption and lifetime properties in a modular fashion. We develop a proof-of-concept implementation by extending CODE CONTRACTS' specification language. To verify the correctness of these annotations we rely on the CODE CONTRACTS static verifier and a points-to analysis. We also briefly discuss possible extensions of our approach to deal with non-linear expressions. © 2014 Pablo F. Castro & Thomas S. E. Maibaum.
Registro:
| Documento: |
Conferencia
|
| Título: | On verifying resource contracts using code contracts |
| Autor: | Castaño, R.; Garbervetsky, D.; Tapicer, J.; Zoppi, E.; Galeotti, J.P.; Ribeiro L.; Aguirre N. |
| Filiación: | Departamento de Computación. FCEyN. UBA, Buenos Aires, Argentina
Saarland University, Saarbrücken, Germany
|
| Palabras clave: | Computational linguistics; Formal methods; Specification languages; Specifications; Dynamic memory; Memory consumption; Memory manager; Points-to analysis; Proof of concept; Resource consumption; Resource usage; Static analyzers; Codes (symbols) |
| Año: | 2014
|
| Volumen: | 139
|
| Página de inicio: | 1
|
| Página de fin: | 15
|
| DOI: |
http://dx.doi.org/10.4204/EPTCS.139.1 |
| Título revista: | 1st Latin American Workshop on Formal Methods, LAFM 2013
|
| Título revista abreviado: | Electron. Proc. Theor. Comput. Sci., EPTCS
|
| ISSN: | 20752180
|
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_20752180_v139_n_p1_Castano |
Referencias:
- Common Compiler Infrastructure, , http://cciast.codeplex.com/
- Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Schlager, S., The key tool (2005) Software & Systems Modeling, 4 (1), pp. 32-54
- Albert, E., Bubel, R., Genaim, S., Hähnle, R., Román-Díez, G., Verified resource guarantees for heap manipulating programs (2012) FASE, pp. 130-145
- Albert, E., Genaim, S., Gómez-Zamalloa, M., Live heap space analysis for languages with garbage collection (2009) ISMM, pp. 129-138
- Albert, E., Genaim, S., Gómez-Zamalloa, M., Heap space analysis for garbage collected languages (2013) Sci. Comput. Program., 78 (9), pp. 1427-1448
- Atkey, R., Amortised resource analysis with separation logic (2011) Logical Methods in Computer Science, 7 (2)
- Barnett, M., Fändrich, M., Garbervetsky, D., Logozzo, F., Annotations for (more) precise points-to analysis (2007) Proceedings of the 2nd International Workshop on Aliasing, Confinement and Ownership in Object-oriented Programming (IWACO'07, pp. 11-18. , http://people.dsv.su.se/~tobias/iwaco/p4-barnett.pdf
- Barthe, G., Pavlova, M., Schneider, G., Precise analysis of memory consumption using program logics (2005) SEFM, pp. 86-95
- Bjorner, N., De Moura, L., (2009) Z3: An Efficient SMT Solver, , http://research.microsoft.com/enus/um/redmond/projects/z3/
- Braberman, V., Fernández, F., Garbervetsky, D., Yovine, S., Parametric prediction of heap memory requirements (2008) Proceedings of the 7th International Symposium on Memory Management, pp. 141-150. , ACM
- Braberman, V.A., Garbervetsky, D., Hym, S., Yovine, S., (2013) Summary-based Inference of Quantitative Bounds of Live Heap Objects, , Submitted
- Chin, W., Hai Nguyen, H., Qin, S., Rinard, M., (2005) Memory Usage Verification for OO Programs, , SAS 05
- Clauss, P., Javier Fernández, F., Garbervetsky, D., Verdoolaege, S., Symbolic polynomial maximization over convex sets and its application to memory requirement estimation (2009) TVLSI, 17 (8), pp. 983-996
- Cousot, P., Cousot, R., Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points (1977) POPL, 77, pp. 238-252
- Fähndrich, M., Barnett, M., Logozzo, F., Embedded contract languages (2010) SAC, 2010, pp. 2103-2110. , ACM
- Fähndrich, M., Logozzo, F., (2009) Clousot: A Language Agnostic Abstract Interpretation-based Static Analyzer for .NET, , http://research.microsoft.com/en-us/people/logozzo/
- Garbervetsky, D., Yovine, S., Braberman, V.A., Rouaux, M., Taboada, A., Quantitative dynamic-memory analysis for Java (2011) Concurrency and Computation: Practice and Experience, 23 (14), pp. 1665-1678
- Gosling, J., Bollella, G., (2000) The Real-Time Specification for Java, , Addison-Wesley Longman Publishing Co., Inc
- Gulwani, S., Zuleger, F., The reachability-bound problem (2010) PLDI'10, pp. 292-304. , ACM
- He, G., Qin, S., Luo, C., Chin, W., Memory usage verification using hip/sleek ATVA'09, pp. 166-181
- Hoffmann, J., Hofmann, M., Amortized resource analysis with polynomial potential (2010) Programming Languages and Systems, pp. 287-306
- Hofman, M., Jost, S., Static prediction of heap usage for first-order functional programs (2003) POPL 03, , SIGPLAN, New Orleans, LA
- Leavens, G.T., Rustan Leino, M.K., Poll, E., Ruby, C., Jacobs, B., JML: Notations and tools supporting detailed design in Java (2000) OOPSLA'00, pp. 105-106
- Meyer, B., Object-oriented software construction (1988) Series in Computer Science, , Prentice-Hall, International, New York
- Meyer, B., (1992) Eiffel: The Language, , Prentice Hall, Hemel HempsteadA4 -
Citas:
---------- APA ----------
Castaño, R., Garbervetsky, D., Tapicer, J., Zoppi, E., Galeotti, J.P., Ribeiro L. & Aguirre N.
(2014)
. On verifying resource contracts using code contracts. 1st Latin American Workshop on Formal Methods, LAFM 2013, 139, 1-15.
http://dx.doi.org/10.4204/EPTCS.139.1---------- CHICAGO ----------
Castaño, R., Garbervetsky, D., Tapicer, J., Zoppi, E., Galeotti, J.P., Ribeiro L., et al.
"On verifying resource contracts using code contracts"
. 1st Latin American Workshop on Formal Methods, LAFM 2013 139
(2014) : 1-15.
http://dx.doi.org/10.4204/EPTCS.139.1---------- MLA ----------
Castaño, R., Garbervetsky, D., Tapicer, J., Zoppi, E., Galeotti, J.P., Ribeiro L., et al.
"On verifying resource contracts using code contracts"
. 1st Latin American Workshop on Formal Methods, LAFM 2013, vol. 139, 2014, pp. 1-15.
http://dx.doi.org/10.4204/EPTCS.139.1---------- VANCOUVER ----------
Castaño, R., Garbervetsky, D., Tapicer, J., Zoppi, E., Galeotti, J.P., Ribeiro L., et al. On verifying resource contracts using code contracts. Electron. Proc. Theor. Comput. Sci., EPTCS. 2014;139:1-15.
http://dx.doi.org/10.4204/EPTCS.139.1
