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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
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)
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)
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)
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)
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 Press
Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA, pp. 14–25 (2000)
Jakob, R., Thiemann, P.: A falsification view of success typings. CoRR, abs/1502.01278 (2015). extended version
Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Asp. Comput. 22(2), 105–128 (2010)
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)
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90. IEEE Computer Society (2006)
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 Press
Reynolds, J.C.: Automatic computation of data set definitions. IFIP Congress 1, 456–461 (1968)
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)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Jakob, R., Thiemann, P. (2015). A Falsification View of Success Typing. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-17524-9_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17523-2
Online ISBN: 978-3-319-17524-9
eBook Packages: Computer ScienceComputer Science (R0)