Abstract
JavaScript ranks among the most popular programming languages for the web, yet its highly dynamic type system and occasionally unintuitive semantics make programming particularly error-prone. This paper presents Javanni, a verifier for JavaScript programs that can statically detect many common programming errors. Javanni checks the absence of standard type-related errors (such as accessing undefined fields) without requiring user-written annotations, and it can also verify full functional-correctness specifications. Several experiments with JavaScript applications reported in the paper demonstrate that Javanni is flexibly usable on programs with non-trivial specifications. Javanni is available online within the CloudStudio web integrated environment.
Chapter PDF
Similar content being viewed by others
References
Anderson, C., Giannini, P., Drossopoulou, S.: Towards Type Inference for JavaScript. In: Gao, X.-X. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 428–452. Springer, Heidelberg (2005)
Gardner, P., Maffeis, S., Smith, G.D.: Towards a program logic for javascript. In: POPL, pp. 31–44 (2012)
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)
Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research (2008)
Nordio, M., et al.: Collaborative software development on the web, arXiv:1105.0768v3 (2011)
Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 382–398. Springer, Heidelberg (2011)
Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Verifying Eiffel programs with Boogie. In: BOOGIE Workshop (2011), http://arxiv.org/abs/1106.4700
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nordio, M., Calcagno, C., Furia, C.A. (2013). Javanni: A Verifier for JavaScript. In: Cortellessa, V., Varró, D. (eds) Fundamental Approaches to Software Engineering. FASE 2013. Lecture Notes in Computer Science, vol 7793. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37057-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-37057-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37056-4
Online ISBN: 978-3-642-37057-1
eBook Packages: Computer ScienceComputer Science (R0)