Relational cost analysis. (English) Zbl 1380.68118
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). 316-329 (2017).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68N18 | Functional programming and lambda calculus |
References:
| [1] | A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In Proceedings of the 15th European Conference on Programming Languages and Systems, ESOP’06, pages 69-83, 2006. 10.1007/11693024_6 · Zbl 1178.68146 |
| [2] | E. Albert, P. Arenas, S. Genaim, M. G´omez-Zamalloa, G. Puebla, D. Ram´ırez, G. Román, and D. Zanardini. Termination and Cost Analysis with COSTA and its User Interfaces. Electr. Notes Theor. Comput. Sci., 258(1):109-121, 2009. 10.1016/j.entcs.2009.12.008 |
| [3] | T. Amtoft, S. Bandhakavi, and A. Banerjee. A logic for information flow in object-oriented programs. In J. G. Morrisett and S. L. P. Jones, editors, Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’06, pages 91-102, 2006. 10.1145/1111037.1111046 · Zbl 1369.68127 |
| [4] | A. W. Appel and D. A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657-683, 2001. 10.1145/504709.504712 |
| [5] | R. Atkey. Amortised Resource Analysis with Separation Logic. In 19th Euro. Symp. on Prog. (ESOP’10), pages 85-103, 2010. 10.1007/978-3-642-11957-6_6 · Zbl 1260.68083 |
| [6] | G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using product programs. In M. J. Butler and W. Schulte, editors, Formal Methods, volume 6664 of Lecture Notes in Computer Science, pages 200-214, 2011. |
| [7] | G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy, and S. Z. Béguelin. Probabilistic relational verification for cryptographic implementations. In S. Jagannathan and P. Sewell, editors, Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’14, pages 193-206, 2014. 10.1145/2535838.2535847 · Zbl 1284.68380 |
| [8] | G. Barthe, M. Gaboardi, E. J. Gallego Arias, J. Hsu, A. Roth, and P.-Y. Strub. Higher-order approximate relational refinement types for mechanism design and differential privacy. In S. K. Rajamani and D. Walker, editors, Proceedings of the 42nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 55-68, 2015. 10.1145/2676726.2677000 · Zbl 1346.68058 |
| [9] | N. Benton. Simple relational correctness proofs for static analyses and program transformations. In N. D. Jones and X. Leroy, editors, Proceedings of the 31th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’04, pages 14-25, 2004. 10.1145/964001.964003 · Zbl 1325.68057 |
| [10] | G. Bonfante, J. Marion, and J. Moyen. Quasi-interpretations a way to control resources. Theor. Comput. Sci., 412(25):2776-2796, 2011. 10.1016/j.tcs.2011.02.007 · Zbl 1230.68077 |
| [11] | M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Alg. for the Constr. and Anal. of Systems - 20th Int. Conf. (TACAS’14), pages 140-155, 2014. |
| [12] | J. Burnim and K. Sen. Asserting and checking determinism for multithreaded programs. In H. van Vliet and V. Issarny, editors, Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009, Amsterdam, The Netherlands, August 24-28, 2009, pages 3-12, 2009. 10.1145/1595696.1595700 |
| [13] | M. Carbin, D. Kim, S. Misailovic, and M. C. Rinard. Proving acceptability properties of relaxed nondeterministic approximate programs. In J. Vitek, H. Lin, and F. Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing, China - June 11 - 16, 2012, pages 169-180, 2012. 10.1145/2254064.2254086 |
| [14] | M. Carbin, S. Misailovic, and M. C. Rinard. Verifying quantitative reliability for programs that execute on unreliable hardware. In A. L. Hosking, P. T. Eugster, and C. V. Lopes, editors, Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, pages 33-52, 2013. 10.1145/2509136.2509546 |
| [15] | Q. Carbonneaux, J. Hoffmann, and Z. Shao. Compositional Certified Resource Bounds. In 36th Conference on Programming Language Design and Implementation (PLDI’15), 2015. Artifact submitted and approved. 10.1145/2737924.2737955 |
| [16] | S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity analysis of programs. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10, pages 57-70, 2010.. 10.1145/1706299.1706308 · Zbl 1312.68056 |
| [17] | E. C ¸ ic¸ek, D. Garg, and U. A. Acar. Refinement types for incremental computational complexity. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, London, UK, April 11-18, 2015. Proceedings, pages 406-431, 2015. · Zbl 1335.68030 |
| [18] | E. C ¸ ic¸ek, Z. Paraskevopoulou, and D. Garg. A type theory for incremental computational complexity with control flow changes. In Proceedings of the 21st International Conference on Functional Programming, ICFP ’16, 2016. 10.1145/2951913.2951950 · Zbl 1361.68062 |
| [19] | M. R. Clarkson and F. B. Schneider. Hyperproperties. In Proceedings of CSF’08, pages 51-65, 2008. 10.1109/CSF.2008.7 |
| [20] | U. Dal Lago and M. Gaboardi. Linear dependent types and relative completeness. In Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science, LICS ’11, pages 133-142, 2011. 10.1109/LICS.2011.22 · Zbl 1261.03073 |
| [21] | U. Dal lago and B. Petit. The geometry of types. In Proceedings of the 40th Annual Symposium on Principles of Programming Languages, POPL ’13, pages 167-178, 2013. 10.1145/2429069.2429090 · Zbl 1301.68184 |
| [22] | N. Danner, D. R. Licata, and R. Ramyaa. Denotational cost semantics for functional languages with inductive types. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 140-151, 2015. 10.1145/2784731.2784749 · Zbl 1360.68323 |
| [23] | D. Felsing, S. Grebing, V. Klebanov, P. Rümmer, and M. Ulbrich. Automating regression verification. In I. Crnkovic, M. Chechik, and P. Grünbacher, editors, ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, Vasteras, Sweden - September 15 - 19, 2014, pages 349-360, 2014.. 10.1145/2642937.2642987 |
| [24] | M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce. Linear dependent types for differential privacy. In Proceedings of the 40th Annual Symposium on Principles of Programming Languages, POPL ’13, pages 357-370, 2013. 10.1145/2429069.2429113 · Zbl 1301.68111 |
| [25] | B. Godlin and O. Strichman. Regression verification: proving the equivalence of similar programs. Softw. Test., Verif. Reliab., 23(3): 241-258, 2013. |
| [26] | S. Gulwani, K. K. Mehra, and T. Chilimbi. Speed: Precise and efficient static estimation of program computational complexity. In Proceedings of the 36th Annual Symposium on Principles of Programming Languages, POPL ’09, pages 127-139, 2009. 10.1145/1480881.1480898 · Zbl 1315.68095 |
| [27] | C. Hawblitzel, S. K. Lahiri, K. Pawar, H. Hashmi, S. Gokbulut, L. Fernando, D. Detlefs, and S. Wadsworth. Will you still compile me tomorrow? static cross-version compiler validation. In B. Meyer, L. Baresi, and M. Mezini, editors, Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, pages 191-201, 2013. 10.1145/2491411.2491442 |
| [28] | J. Hoffmann and Z. Shao. Automatic Static Cost Analysis for Parallel Programs. In 24th European Symposium on Programming (ESOP’15), 2015. 10.1007/978-3-662-46669-8_6 · Zbl 1335.68056 |
| [29] | J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. In Proceedings of the 38th Annual Symposium on Principles of Programming Languages, POPL ’11, pages 357-370, 2011. 10.1145/1926385.1926427 · Zbl 1284.68132 |
| [30] | J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. ACM Trans. Program. Lang. Syst., 2012. 10.1145/2362389.2362393 · Zbl 1284.68132 |
| [31] | S. K. Lahiri, K. Vaswani, and C. A. R. Hoare. Differential static analysis: opportunities, applications, and challenges. In G. Roman and K. J. Sullivan, editors, Proceedings of the Workshop on Future of Software Engineering Research, FoSER 2010, at the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, Santa Fe, NM, USA, November 7-11, 2010, pages 201-204, 2010.. 10.1145/1882362.1882405 |
| [32] | S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebˆelo. SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In P. Madhusudan and S. A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, volume 7358 of Lecture Notes in Computer Science, pages 712-717, 2012. 10.1007/978-3-642-31424-7_54 |
| [33] | S. K. Lahiri, K. L. McMillan, R. Sharma, and C. Hawblitzel. Differential assertion checking. In B. Meyer, L. Baresi, and M. Mezini, editors, Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, pages 345-355, 2013. 10.1145/2491411.2491452 |
| [34] | F. Logozzo, S. K. Lahiri, M. Fähndrich, and S. Blackshear. Verification modulo versions: towards usable verification. In M. F. P. O’Boyle and K. Pingali, editors, Proceedings of 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’14, page 32, 2014. 10.1145/2594291.2594326 |
| [35] | A. Nanevski, A. Banerjee, and D. Garg. Verification of information flow and access control policies with dependent types. In 32nd IEEE Symposium on Security and Privacy, S&P 2011, 22-25 May 2011, Berkeley, California, USA, pages 165-179, 2011. 10.1109/SP.2011.12 |
| [36] | F. Nielson and H. Nielson. Type and effect systems. In Correct System Design, volume 1710 of Lecture Notes in Computer Science, pages 114-136. 1999. |
| [37] | N. Partush and E. Yahav. Abstract semantic differencing via speculative correlation. In A. P. Black and T. D. Millstein, editors, Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, pages 811-828, 2014. 10.1145/2660193.2660245 |
| [38] | S. Person, M. B. Dwyer, S. G. Elbaum, and C. S. Pasareanu. Differential symbolic execution. In M. J. Harrold and G. C. Murphy, editors, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008, Atlanta, Georgia, USA, November 9-14, 2008, pages 226-237, 2008. 10.1145/1453101.1453131 |
| [39] | S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed incremental symbolic execution. In M. W. Hall and D. A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 504-515, 2011. 10.1145/1993498.1993558 |
| [40] | F. Pottier and V. Simonet. Information flow inference for ML. ACM Trans. Prog. Lang. Sys., 25(1):117-158, Jan. 2003. 10.1145/596980.596983 · Zbl 1323.68148 |
| [41] | J. Reed and B. C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 157- 168, 2010. 10.1145/1863543.1863568 · Zbl 1323.68254 |
| [42] | B. Reistad and D. K. Gifford. Static dependent costs for estimating execution time. In Proceedings of the 1994 ACM Conference on LISP and Functional Programming, LFP ’94, pages 65-78, 1994. 10.1145/182409.182439 |
| [43] | D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 221-232, 1995. 10.1145/199448.199485 |
| [44] | M. Sinn, F. Zuleger, and H. Veith. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification - 26th Int. Conf. (CAV’14), page 743-759, 2014. 10.1007/978-3-319-08867-9_50 |
| [45] | T. Terauchi and A. Aiken. Secure information flow as a safety problem. In C. Hankin and I. Siveroni, editors, Static Analysis Symposium, volume 3672, pages 352-367, 2005. 10.1007/11547662_24 · Zbl 1141.68380 |
| [46] | G. Yang, M. B. Dwyer, and G. Rothermel. Regression model checking. In 25th IEEE International Conference on Software Maintenance (ICSM 2009), September 20-26, 2009, Edmonton, Alberta, Canada, pages 115-124, 2009. |
| [47] | H. Yang. Relational separation logic. Theoretical Comput. Sci., 375 (1-3):308-334, 2007. 10.1016/j.tcs.2006.12.036 · Zbl 1111.68078 |
| [48] | A. Zaks and A. Pnueli. CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In J. Cuéllar, T. S. E. Maibaum, and K. Sere, editors, Formal Methods, volume 5014 of Lecture Notes in Computer Science, pages 35-51, 2008. 10.1007/978-3-540-68237-0_5 |
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.
