We present an approach to automatic checking of the correctness of web applications structure during their life-cycle. The approach adopts the well-established symbolic model checking technique and the associated tool SMV [13]. A formalism allows the designer to describe the model of a web-based system. Computation Tree Logic (CTL) is adopted as language to define the properties to be verified. The approach has been implemented in a tool to provide automatic support in the design of web applications. The system embeds the NuSMV [1] model checker to perform verification. Verification is carried out after building the finite state model of a site in the model checker input language. To this purpose the system parses the HTML source code of web pages, including code for dynamic pages. Properties are expressed using a user friendly interface for web application developers that automatically translates properties in CTL formulas.