The Community for Technology Leaders
2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) (2004)
Linz, Austria
Sept. 20, 2004 to Sept. 24, 2004
ISSN: 1068-3062
ISBN: 0-7695-2131-2
pp: 164-173
Daniel R. Licata , Brown University
Shriram Krishnamurthi , Brown University
ABSTRACT
Web programs are important, increasingly representing the primary public interfaces of commercial organizations. Unfortunately, Web programs also exhibit numerous flaws. In addition to the usual correctness problems faced by software, Web programs must contend with numerous subtle user operations such as clicking the Back button or cloning and submitting a page multiple times. Many existing Web verification tools fail to even consider, much less effectively handle, these operations.<div></div> This paper describes a model checker designed to identify errors in Web software. We present a technique for automatically generating novel models of Web programs from their source code; these models include the additional control flow enabled by these user operations. In this technique, we exploit a constraint-based approach to avoid overapproximating this control flow; this approach allows us to evade exploding the size of the model. Further, we present a powerful base property language that permits specification of useful Web properties, along with several property idioms that simplify specification of the most common Web properties. Finally, we discuss the implementation of this model checker and a study of its effectiveness.
INDEX TERMS
null
CITATION
Daniel R. Licata, Shriram Krishnamurthi, "Verifying Interactive Web Programs", 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), vol. 00, no. , pp. 164-173, 2004, doi:10.1109/ASE.2004.10054
96 ms
(Ver 3.3 (11022016))