Skip to main content
SpringerLink
Log in

Towards Logic-Based Verification of JavaScript Programs

  • Conference paper
  • First Online:
Automated Deduction – CADE 26 (CADE 2017)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10395))

Included in the following conference series:

Abstract

In this position paper, we argue for what we believe is a correct pathway to achieving scalable symbolic verification of JavaScript based on separation logic. We highlight the difficulties imposed by the language, the current state-of-the-art in the literature, and the sequence of steps that needs to be taken. We briefly describe , our semi-automatic toolchain for JavaScript verification.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

Notes

  1. 1.

    The formal result that the compiler is semantics-preserving has been done for a fragment of the language.

References

  1. Andreasen, E., Møller, A.: Determinacy in static analysis for jQuery. In: OOPSLA (2014)

    Google Scholar 

  2. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006). doi:10.1007/11804192_6

    Chapter  Google Scholar 

  3. Berdine, J., Cook, B., Ishtiaq, S.: Slayer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_15

    Chapter  Google Scholar 

  4. Bodin, M., Charguéraud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaScript specification. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 87–100. ACM Press (2014)

    Google Scholar 

  5. Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, 8–10 December 2008, San Diego, California, USA, Proceedings, pp. 209–224. USENIX Association (2008)

    Google Scholar 

  6. Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O’Hearn, P., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). doi:10.1007/978-3-319-17524-9_1

    Google Scholar 

  7. Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009)

    Google Scholar 

  8. Ştefănescu, A., Park, D., Yuwen, S., Li, Y., Roşu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 31th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016), pp. 74–91. ACM, November 2016

    Google Scholar 

  9. Distefano, D., Parkinson, M.: jStar: towards practical verification for Java. In: OOPSLA (2008)

    Google Scholar 

  10. ECMAScript Committee. The 5th edn. of the ECMAScript Language Specification. Technical report, ECMA (2011)

    Google Scholar 

  11. ECMAScript Committee. Test262 test suite (2017). https://github.com/tc39/test262

  12. Fink, S., Dolby, J.: WALA – The T.J. Watson Libraries for Analysis (2015). http://wala.sourceforge.net/

  13. Gardner, P., Maffeis, S., Smith, G.: Towards a program logic for JavaScript. In: Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 31–44. ACM Press (2012)

    Google Scholar 

  14. Guha, A., Saftoiu, C., Krishnamurthi, S.: The essence of JavaScript. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 126–150. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14107-2_7

    Chapter  Google Scholar 

  15. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). doi:10.1007/978-3-642-20398-5_4

    Chapter  Google Scholar 

  16. JaVerT Team. Javert (2017). http://goo.gl/au69SV

  17. Jensen, S.H., Møller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 238–255. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03237-0_17

    Chapter  Google Scholar 

  18. Jones, J.: Priority queue data structure (2016). https://github.com/jasonsjones/queue-pri

  19. Kashyap, V., Dewey, K., Kuefner, E.A., Wagner, J., Gibbons, K., Sarracino, J., Wiedermann, B., Hardekopf, B.: JSAI: a static analysis platform for JavaScript. In: FSE, pp. 121–132 (2014)

    Google Scholar 

  20. Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_26

    Chapter  Google Scholar 

  21. Livshits, B.: JSIR, an intermediate representation for JavaScript analysis (2014). http://too4words.github.io/jsir/

  22. Park, D., Stefănescu, A., Roşu, G.: KJS: a complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, New York, USA, pp. 346–356. ACM (2015)

    Google Scholar 

  23. Politz, J.G., Carroll, M.J., Lerner, B.S., Pombrio, J., Krishnamurthi, S.: A tested semantics for getters, setters, and eval in JavaScript. In: Proceedings of the 8th Symposium on Dynamic Languages (2012)

    Google Scholar 

  24. Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397–434 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  25. Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested hoare triples and frame rules for higher-order store. Logical Methods Comput. Sci. 7(3), 1–42 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  26. Sridharan, M., Dolby, J., Chandra, S., Schäfer, M., Tip, F.: Correlation tracking for points-to analysis of JavaScript. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 435–458. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31057-7_20

    Chapter  Google Scholar 

  27. Visser, W., Pǎsǎreanu, C.S., Khurshid, S.: Test input generation with java pathfinder. In: Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, New York, USA, pp. 97–107. ACM (2004)

    Google Scholar 

Download references

Acknowledgments

Fragoso Santos, Gardner, and Maksimović were supported by the EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems (EP/K008528/1), and the Department of Computing in Imperial College London. Naudžiūnienė was supported by an EPSRC DTA award. Maksimović was also partially supported by the Serbian Ministry of Education and Science through the Mathematical Institute of Serbian Academy of Sciences and Arts, projects ON174026 and III44006.

Author information

Authors and Affiliations

  1. Imperial College London, London, UK

    José Fragoso Santos, Philippa Gardner, Petar Maksimović & Daiva Naudžiūnienė

  2. Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade, Serbia

    Petar Maksimović

Authors
  1. José Fragoso Santos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Philippa Gardner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Petar Maksimović
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Daiva Naudžiūnienė
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Petar Maksimović .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Leonardo de Moura

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Santos, J.F., Gardner, P., Maksimović, P., Naudžiūnienė, D. (2017). Towards Logic-Based Verification of JavaScript Programs. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63046-5_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63045-8

  • Online ISBN: 978-3-319-63046-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation