Web Verification: Perspective and Challenges

The Web poses novel and interesting problems for both programming language design and verification--and their intersection. This paper provides a personal outline of one thread of work on this topic. Key words: Web applications, temporal verification, access control, program analysis 1 What is a Web Site? The term "Web site" contains a hidden ambiguity. Is a site a static entity, to be viewed as a program source, or is it a dynamic entity, to be viewed through the lens of user behavior? This distinction significantly impacts what it means to analyze and verify a Web site. All the traditional trade-offs between static and dynamic analyses apply: a static analysis can quantify over all program behaviors, but will usually be less specific; a dynamic analysis can only offer guarantees relative to the behaviors it has examined, but the additional contextual information can often yield more informative answers. This distinction potentially matters more on the Web, due to the natur...

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Shriram Krishnamurthi
• Keywords: ENTCS 2006, Web Applications, Web Interactions, Web Sites