Advertisement

Type-Directed Bounding of Collections in Reactive Programs

  • Tianhan LuEmail author
  • Pavol Černý
  • Bor-Yuh Evan Chang
  • Ashutosh Trivedi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)

Abstract

Our aim is to statically verify that in a given reactive program, the length of collection variables does not grow beyond a given bound. We propose a scalable type-based technique that checks that each collection variable has a given refinement type that specifies constraints about its length. A novel feature of our refinement types is that the refinements can refer to AST counters that track how many times an AST node has been executed. This feature enables type refinements to track limited flow-sensitive information. We generate verification conditions that ensure that the AST counters are used consistently, and that the types imply the given bound. The verification conditions are discharged by an off-the-shelf SMT solver. Experimental results demonstrate that our technique is scalable, and effective at verifying reactive programs with respect to requirements on length of collections.

References

  1. 1.
    DARPA space-time analysis for cybersecurity program (STAC). http://www.darpa.mil/program/space-time-analysis-for-cybersecurity
  2. 2.
    Scala library for parsing and printing the SMT-LIB format. https://github.com/regb/scala-smtlib
  3. 3.
    Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of Java bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71316-6_12CrossRefGoogle Scholar
  4. 4.
    Albert, E., Genaim, S., Gomez-Zamalloa, M.: Heap space analysis for Java bytecode. In: Proceedings of the 6th International Symposium on Memory Management, pp. 105–116. ACM (2007)Google Scholar
  5. 5.
    Albert, E., Genaim, S., Gómez-Zamalloa Gil, M.: Live heap space analysis for languages with garbage collection. In: Proceedings of the 2009 International Symposium on Memory Management, pp. 129–138. ACM (2009)Google Scholar
  6. 6.
    Albert, E., Genaim, S., Masud, A.N.: More precise yet widely applicable cost analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 38–53. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_5CrossRefGoogle Scholar
  7. 7.
    Alonso-Blas, D.E., Genaim, S.: On the limits of the classical approach to cost analysis. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 405–421. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33125-1_27CrossRefGoogle Scholar
  8. 8.
    Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. ACM SIGPLAN Not. 50(6), 467–478 (2015)CrossRefGoogle Scholar
  9. 9.
    Chin, W.N., Khoo, S.C.: Calculating sized types. High.-Order Symb. Comput. 14(2–3), 261–300 (2001)CrossRefGoogle Scholar
  10. 10.
    Coughlin, D., Chang, B.Y.E.: Fissile type analysis: modular checking of almost everywhere invariants. ACM SIGPLAN Not. 49, 73–85 (2014)CrossRefGoogle Scholar
  11. 11.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  12. 12.
    Dietl, W., Dietzel, S., Ernst, M.D., Muşlu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 681–690. ACM (2011)Google Scholar
  13. 13.
    Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275–295. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-12736-1_15CrossRefGoogle Scholar
  14. 14.
    Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184–191. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08587-6_13CrossRefGoogle Scholar
  15. 15.
    Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. ACM SIGPLAN Not. 44, 375–385 (2009)CrossRefGoogle Scholar
  16. 16.
    Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. ACM SIGPLAN Not. 44, 127–139 (2009)CrossRefGoogle Scholar
  17. 17.
    Gulwani, S., Zuleger, F.: The reachability-bound problem. ACM SIGPLAN Not. 45, 292–304 (2010)CrossRefGoogle Scholar
  18. 18.
    Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM SIGPLAN Not. 46, 357–370 (2011)CrossRefGoogle Scholar
  19. 19.
    Hoffmann, J., Das, A., Weng, S.C.: Towards automatic resource bound analysis for OCaml. ACM SIGPLAN Not. 52, 359–373 (2017)CrossRefGoogle Scholar
  20. 20.
    Olivo, O., Dillig, I., Lin, C.: Static detection of asymptotic performance bugs in collection traversals. ACM SIGPLAN Not. 50, 369–378 (2015)CrossRefGoogle Scholar
  21. 21.
    Papi, M.M., Ali, M., Correa Jr., T.L., Perkins, J.H., Ernst, M.D.: Practical pluggable types for Java. In: Proceedings of the 2008 International Symposium on Software Testing and Analysis, pp. 201–212. ACM (2008)Google Scholar
  22. 22.
    Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. ACM SIGPLAN Not. 43, 159–169 (2008)CrossRefGoogle Scholar
  23. 23.
    Rondon, P.M., Kawaguchi, M., Jhala, R.: Low-level liquid types. ACM SIGPLAN Not. 45, 131–144 (2010)CrossRefGoogle Scholar
  24. 24.
    Sinn, M., Zuleger, F., Veith, H.: A simple and scalable approach to bound analysis and amortized complexity analysis. In: Computer Aided Verification-26th International Conference (CAV 14), pp. 743–759 (2014)Google Scholar
  25. 25.
    Vasconcelos, P.B.: Space cost analysis using sized types. Ph.D. thesis, University of St Andrews (2008)Google Scholar
  26. 26.
    Vasconcelos, P.B., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: Trinder, P., Michaelson, G.J., Peña, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 86–101. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27861-0_6CrossRefzbMATHGoogle Scholar
  27. 27.
    Lu, T., Cerný, P., Chang, B.-Y.E., Trivedi, A.: Type-directed bounding of collections in reactive programs. CoRR abs/1810.10443 (2018)Google Scholar
  28. 28.
    Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)zbMATHGoogle Scholar
  29. 29.
    Xu, G., Rountev, A.: Precise memory leak detection for Java software using container profiling. In: Proceedings of the 30th International Conference on Software Engineering, pp. 151–160. ACM (2008)Google Scholar
  30. 30.
    Xu, G., Rountev, A.: Detecting inefficiently-used containers to avoid bloat. ACM SIGPLAN Not. 45, 160–173 (2010)CrossRefGoogle Scholar
  31. 31.
    Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-23702-7_22CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Tianhan Lu
    • 1
    Email author
  • Pavol Černý
    • 1
  • Bor-Yuh Evan Chang
    • 1
  • Ashutosh Trivedi
    • 1
  1. 1.University of Colorado BoulderBoulderUSA

Personalised recommendations