Advertisement

A Falsification View of Success Typing

  • Robert JakobEmail author
  • Peter Thiemann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)

Abstract

Dynamic languages are praised for their flexibility and expressiveness, but static analysis often yields many false positives and verification is cumbersome for lack of structure. Hence, unit testing is the prevalent incomplete method for validating programs in such languages.

Falsification is an alternative approach that uncovers definite errors in programs. A falsifier computes a set of inputs that definitely crash a program.

Success typing is a type-based approach to document programs in dynamic languages. We demonstrate that success typing is, in fact, an instance of falsification by mapping success (input) types into suitable logic formulae. Output types are represented by recursive types. We prove the correctness of our mapping (which establishes that success typing is falsification) and we report some experiences with a prototype implementation.

Keywords

Model Check Function Application Output Type Tree Automaton Constructor Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 67–81. Springer, Heidelberg (2005) CrossRefGoogle Scholar
  2. 2.
    Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Gros, C., Kamsky, A., McPeak, S., Engler, D.R.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66–75 (2010)CrossRefGoogle Scholar
  3. 3.
    Bodin, M., Charguéraud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaSript specification. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 87–100. ACM (2014)Google Scholar
  4. 4.
    Cartwright, R., Fagan, M.: Soft typing. In: Wise, D.S. (ed.) Proceedings of the ACM SIGPLAN’91 PLDI, Toronto, Ontario, Canada, June 26–28, 1991, pp. 278–292 (1991)Google Scholar
  5. 5.
    Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a SAT solver. In: Crnkovic, I., Bertolino, A. (eds.) Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007, Dubrovnik, Croatia, September 3–7, 2007, pp. 195–204. ACM (2007)Google Scholar
  6. 6.
    Gardner, P., Maffeis, S., Smith, G.D.: Towards a program logic for JavaScript. In: Field, J., Hicks, M. (eds.) Proc. 39th ACM Symp. POPL, pp. 31–44, Philadelphia, USA, January 2012. ACM PressGoogle Scholar
  7. 7.
    Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA, pp. 14–25 (2000)Google Scholar
  8. 8.
    Jakob, R., Thiemann, P.: A falsification view of success typings. CoRR, abs/1502.01278 (2015). extended versionGoogle Scholar
  9. 9.
    Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Asp. Comput. 22(2), 105–128 (2010)CrossRefzbMATHGoogle Scholar
  10. 10.
    Lindahl, T., Sagonas, K.F.: Practical type inference based on success typings. In: Bossi, A., Maher, M.J. (eds.) PPDP, pp. 167–178. ACM (2006)Google Scholar
  11. 11.
    Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90. IEEE Computer Society (2006)Google Scholar
  12. 12.
    Ong, C.-H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 587–598, Austin, TX, USA, January 2011. ACM PressGoogle Scholar
  13. 13.
    Reynolds, J.C.: Automatic computation of data set definitions. IFIP Congress 1, 456–461 (1968)Google Scholar
  14. 14.
    Sagonas, K.F., Silva, J., Tamarit, S.: Precise explanation of success typing errors. In: Albert, E., Mu, S.-C. (eds.) PEPM, pp. 33–42. ACM (2013)Google Scholar
  15. 15.
    Taghdiri, M.: Inferring specifications to detect errors in code. In: 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20–25 September 2004, Linz, Austria, pp. 144–153. IEEE Computer Society (2004)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.University of FreiburgFreiburgGermany

Personalised recommendations