3. Organization

The remainder of this paper is organized as follows. Section 2 introduces program checking and describes how checklets (program checkers in A$\lambda$goVista) are used as the basic entries in A$\lambda$goVista's database. Section 3 presents the overall architecture of A$\lambda$goVista and discusses relevant security issues. Section 4 describes the design of the A$\lambda$goVista query language and type system. Section 5 introduces query transformations that the system uses to bridge any potential semantic gap between user queries and checklets. Section 6 discusses checklet design issues. Section 7 describes how advanced type analysis can speed up searching, and Section 8 evaluates the performance of the search algorithms. Section 9 discusses related work, and Section 10, finally, summarizes our results.