Towards automatic resource bound analysis for OCaml. (English) Zbl 1380.68123
Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 359-373 (2017).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68N15 | Theory of programming languages |
| 68N20 | Theory of compilers and interpreters |
Keywords:
amortized analysis; LP-solving; resource-bound analysis; static analysis; type inference; type systemsReferences:
| [1] | E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In 16th European Symposium on Programming (ESOP’07), pages 157-172, 2007. · Zbl 1236.68042 |
| [2] | E. Albert, P. Arenas, S. Genaim, and G. Puebla. Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning, pages 161-203, 2011. 10.1007/s10817-010-9174-1 · Zbl 1213.68200 |
| [3] | E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, and G. Puebla. Automatic Inference of Resource Consumption Bounds. In Logic for Programming, Artificial Intelligence, and Reasoning, 18th Conference (LPAR’12), pages 1-11, 2012. 10.1007/978-3-642-28717-6_1 · Zbl 1352.68048 |
| [4] | E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Object-Oriented Bytecode Programs. Theoretical Computer Science, 413(1):142 - 159, 2012. 10.1016/j.tcs.2011.07.009 · Zbl 1236.68042 |
| [5] | E. Albert, J. C. Fernández, and G. Román-Díez. Non-cumulative Resource Analysis. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, (TACAS’15), pages 85-100, 2015. 10.1007/978-3-662-46681-0_6 |
| [6] | C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In 17th International Static Analysis Symposium (SAS’10), pages 117-133, 2010. · Zbl 1306.68017 |
| [7] | D. E. Alonso-Blas and S. Genaim. On the limits of the classical approach to cost analysis. In 19th International Static Analysis Symposium (SAS’12), pages 405-421, 2012. 10.1007/978-3-642-33125-1_27 |
| [8] | R. Atkey. Amortised Resource Analysis with Separation Logic. In 19th European Symposium on Programming (ESOP’10), pages 85-103, 2010. 10.1007/978-3-642-11957-6_6 · Zbl 1260.68083 |
| [9] | M. Avanzini and G. Moser. A Combination Framework for Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA’13), pages 55-70, 2013. · Zbl 1356.68092 |
| [10] | M. Avanzini, U. D. Lago, and G. Moser. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In 29th International Conference on Functional Programming (ICFP’15), pages 152-164, 2012. 10.1145/2784731.2784753 · Zbl 1360.68313 |
| [11] | R. Benzinger. Automated Higher-Order Complexity Analysis. Theoretical Computer Science, 318(1-2):79-103, 2004. 10.1016/j.tcs.2003.10.022 · Zbl 1071.68029 |
| [12] | R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács. ABC: Algebraic Bound Computation for Loops. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference (LPAR’10), pages 103-118, 2010. · Zbl 1253.68093 |
| [13] | G. E. Blelloch and J. Greiner. A Provable Time and Space Efficient Implementation of NESL. In First International Conference on Functional Programming (ICFP’96), pages 213-225, 1996. 10.1145/232627.232650 · Zbl 1344.68048 |
| [14] | G. E. Blelloch and R. Harper. Cache and I/O Efficent Functional Algorithms. In 40th Symposium on Principles of Programming Languages (POPL’13), pages 39-50, 2013. 10.1145/2429069.2429077 · Zbl 1301.68175 |
| [15] | M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference (TACAS’14), pages 140-155, 2014. |
| [16] | B. Campbell. Amortised Memory Analysis using the Depth of Data Structures. In 18th European Symposium on Programming (ESOP’09), pages 190-204, 2009. 10.1007/978-3-642-00590-9_14 · Zbl 1234.68072 |
| [17] | Q. Carbonneaux, J. Hoffmann, and Z. Shao. Compositional Certified Resource Bounds. In 36th Conference on Programming Language Design and Implementation (PLDI’15), pages 467-478, 2015. 10.1145/2737924.2737955 |
| [18] | P. Cerný, T. A. Henzinger, L. Kovács, A. Radhakrishna, and J. Zwirchmayr. Segment Abstraction for Worst-Case Execution Time Analysis. In 24th European Symposium on Programming (ESOP’15), pages 105- 131, 2015. · Zbl 1335.68049 |
| [19] | E. Çiçek, D. Garg, and U. A. Acar. Refinement Types for Incremental Computational Complexity. In 24th European Symposium on Programming (ESOP’15), pages 406-431, 2015. · Zbl 1335.68030 |
| [20] | K. Crary and S. Weirich. Resource Bound Certification. In 27th Symposium on Principles of Programming Languages (POPL’00), pages 184-198, 2000. 10.1145/325694.325716 · Zbl 1323.68368 |
| [21] | S. A. Crosby and D. S. Wallach. Denial of service via algorithmic complexity attacks. In 12th USENIX Security Symposium (USENIX’12), pages 3-3, 2003. |
| [22] | N. A. Danielsson. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th Symposium on Principles of Programming Languauges (POPL’08), pages 133-144, 2008. 10.1145/1328438.1328457 · Zbl 1295.68060 |
| [23] | N. Danner, D. R. Licata, and R. Ramyaa. Denotational Cost Semantics for Functional Languages with Inductive Types. In 29th International Conference on Functional Programming (ICFP’15), pages 140-151, 2012. 10.1145/2784731.2784749 · Zbl 1360.68323 |
| [24] | N. Danner, J. Paykin, and J. S. Royer. A Static Cost Analysis for a Higher-Order Language. In 7th Workshop on Programming Languages Meets Program Verification (PLPV’13), pages 25-34, 2013. 10.1145/2428116.2428123 |
| [25] | A. Flores-Montoya and R. Hähnle. Resource Analysis of Complex Programs with Cost Equations. In Programming Languages and Systems - 12th Asian Symposium (APLAS’14), pages 275-295, 2014. · Zbl 1453.68047 |
| [26] | B. Grobauer. Cost Recurrences for DML Programs. In 6th International Conference on Functional Programming (ICFP’01), pages 253-264, 2001. 10.1145/507635.507666 · Zbl 1323.68118 |
| [27] | S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In 36th Symposium on Principles of Programming Languauges (POPL’09), pages 127-139, 2009. 10.1145/1480881.1480898 · Zbl 1315.68095 |
| [28] | J. Hoffmann. RAML Web Site. http://raml.co, 2016. |
| [29] | J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polynomial Potential. In 19th European Symposium on Programming (ESOP’10), pages 287-306, 2010. 10.1007/978-3-642-11957-6_16 · Zbl 1260.68074 |
| [30] | J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics. In Programming Languages and Systems - 8th Asian Symposium (APLAS’10), pages 172-187, 2010. |
| [31] | J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. In 38th Symposium on Principles of Programming Languages (POPL’11), pages 357-370, 2011. 10.1145/1926385.1926427 · Zbl 1284.68132 |
| [32] | J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. ACM Transactions on Programming Languages and Systems, 34:14:1-14:62, 2012. 10.1145/2362389.2362393 · Zbl 1284.68132 |
| [33] | J. Hoffmann, A. Das, and S.-C. Weng. Towards Automatic Resource Bound Analysis for OCaml. ArXiv e-prints, 2016. |
| [34] | M. Hofmann and S. Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In 30th Symposium on Principles of Programming Languages (POPL’03), pages 185-197, 2003. 10.1145/604131.604148 · Zbl 1321.68180 |
| [35] | M. Hofmann and S. Jost. Type-Based Amortised Heap-Space Analysis. In 15th European Symposium on Programming (ESOP’06), pages 22- 37, 2006. 10.1007/11693024_3 · Zbl 1178.68143 |
| [36] | M. Hofmann and G. Moser. Amortised Resource Analysis and Typed Polynomial Interpretations. In Rewriting and Typed Lambda Calculi (RTA-TLCA;14), pages 272-286, 2014. · Zbl 1416.68093 |
| [37] | M. Hofmann and G. Moser. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA’15), pages 241-256, 2015. · Zbl 1367.68138 |
| [38] | M. Hofmann and D. Rodriguez. Automatic Type Inference for Amortised Heap-Space Analysis. In 22nd European Symposium on Programming (ESOP’13), pages 593-613, 2013. 10.1007/978-3-642-37036-6_32 · Zbl 1381.68041 |
| [39] | J. Hughes, L. Pareto, and A. Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In 23rd Symposium on Principles of Programming Languages (POPL’96), pages 410-423, 1996. 10.1145/237721.240882 |
| [40] | G. Jin, L. Song, X. Shi, J. Scherpelz, and S. Lu. Understanding and Detecting Real-World Performance Bugs. In 33rd Conference on Programming Language Design and Implementation PLDI’12, pages 77-88, 2012. 10.1145/2254064.2254075 |
| [41] | S. Jost, K. Hammond, H.-W. Loidl, and M. Hofmann. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In 37th Symposium on Principles of Programming Languages (POPL’10), pages 223-236, 2010. 10.1145/1706299.1706327 · Zbl 1312.68039 |
| [42] | P. C. Kocher. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In Advances in Cryptology - 16th Annual International Cryptology Conference (CRYPTO’96), pages 104- 113, 1996. · Zbl 1329.94070 |
| [43] | U. D. Lago and M. Gaboardi. Linear Dependent Types and Relative Completeness. In 26th IEEE Symposium on Logic in Computer Science (LICS’11), pages 133-142, 2011. 10.1109/LICS.2011.22 · Zbl 1261.03073 |
| [44] | U. D. Lago and B. Petit. The Geometry of Types. In 40th Symposium on Principles of Programming Languages (POPL’13), pages 167-178, 2013. 10.1145/2429069.2429090 · Zbl 1301.68184 |
| [45] | X. Leroy. The ZINC Experiment: An Economical Implementation of the ML Language. Technical report 117, INRIA, 1990. |
| [46] | X. Leroy. From Krivine’s Machine to the Caml Implementation. http://pauillac.inria.fr/ xleroy/talks/zam-kazam05.pdf, 2005. Invited talk, May 17, Workshop on the Krivine and ZINC Abstract Machines. |
| [47] | X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7):107-115, 2009. 10.1145/1538788.1538814 |
| [48] | X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy, and J. Vouillon. The OCaml system release 4.02. Technical report, Institut National de Recherche en Informatique et en Automatique, 2014. |
| [49] | V. Nicollet. 99 problems (solved) in ocaml. https://ocaml.org/ learn/tutorials/99problems.html, 2016. |
| [50] | L. Noschinski, F. Emmes, and J. Giesl. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. Journal of Automated Reasoning, 51(1):27-56, 2013. · Zbl 1314.68174 |
| [51] | O. Olivo, I. Dillig, and C. Lin. Static Detection of Asymptotic Performance Bugs in Collection Traversals. In Conference on Programming Language Design and Implementation (PLDI’15), pages 369-378, 2015. 10.1145/2737924.2737966 |
| [52] | H. R. Simões, P. B. Vasconcelos, M. Florido, S. Jost, and K. Hammond. Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs. In 17th International Conference on Functional Programming (ICFP’12), pages 165-176, 2012. 10.1145/2364527.2364575 · Zbl 1291.68027 |
| [53] | M. Sinn, F. Zuleger, and H. Veith. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification - 26th International Conference (CAV’14), page 743-759, 2014. 10.1007/978-3-319-08867-9_50 |
| [54] | R. E. Tarjan. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods, 6(2):306-318, 1985. · Zbl 0599.68046 |
| [55] | R. J. Vanderbei. Linear Programming: Foundations and Extensions. Springer US, 2001. · Zbl 1043.90002 |
| [56] | P. Vasconcelos. Space Cost Analysis Using Sized Types. PhD thesis, School of Computer Science, University of St Andrews, 2008. |
| [57] | P. B. Vasconcelos and K. Hammond. Inferring Costs for Recursive, Polymorphic and Higher-Order Functional Programs. In 15th International Conference on Implementation of Functional Languages (IFL’03), pages 86-101, 2003. 10.1007/978-3-540-27861-0_6 · Zbl 1108.68356 |
| [58] | P. B. Vasconcelos, S. Jost, M. Florido, and K. Hammond. Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages. In 24th European Symposium on Programming (ESOP’15), pages 787- 811, 2015. · Zbl 1335.68035 |
| [59] | B. Wegbreit. Mechanical Program Analysis. Communications of the ACM, 18(9):528-539, 1975. 10.1145/361002.361016 · Zbl 0306.68008 |
| [60] | F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th International Static Analysis Symposium (SAS’11), pages 280-297, 2011. |
| [61] | E. Çiçek, G. Barthe, M. Gaboardi, D. Garg, and J. Hoffmann. Relational Cost Analysis. In 44th Symposium on Principles of Programming Languages (POPL’17), 2017. Forthcoming. 10.1145/3009837.3009858 · Zbl 1380.68118 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
