Skip to main content
SpringerLink
Log in

A Falsification View of Success Typing

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9058))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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)

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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. 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. 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. 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

    Google Scholar 

  7. Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA, pp. 14–25 (2000)

    Google Scholar 

  8. Jakob, R., Thiemann, P.: A falsification view of success typings. CoRR, abs/1502.01278 (2015). extended version

    Google Scholar 

  9. Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Asp. Comput. 22(2), 105–128 (2010)

    Article  MATH  Google Scholar 

  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. 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. 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

    Google Scholar 

  13. Reynolds, J.C.: Automatic computation of data set definitions. IFIP Congress 1, 456–461 (1968)

    Google Scholar 

  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. 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 

Download references

Author information

Authors and Affiliations

  1. University of Freiburg, Freiburg, Germany

    Robert Jakob & Peter Thiemann

Authors
  1. Robert Jakob
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Thiemann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Robert Jakob .

Editor information

Editors and Affiliations

  1. Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. Jet Propulsion Laboratory, Pasadena, California, USA

    Gerard Holzmann

  3. Jet Propulsion Laboratory, Pasadena, California, USA

    Rajeev Joshi

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation