Mark P. Jones. In Proceedings of the 2005 Automated Software Engineering Workshop on Software Certificate Management (SoftCeMent '05), Long Beach, CA, November 2005.
This paper summarizes our efforts in the Programatica project at OGI and PSU to design new kinds of tools to support the development and certification of software systems. Our approach relies on a tight integration of program source code, embedded formal properties, and associated evidence of validity. A particular goal for the toolset is to facilitate efficient and effective use of many different kinds of evidence during pro ject development. Our current prototype targets validation of functional (security) properties of programs written in Haskell. This tool provides connections, through a language of formal properties called P-logic, to several external validation tools and supports unit testing, random testing, automated and interactive theorem proving, and signed assertions. The underlying concepts, however, are quite general and should be easily adaptable to other programming languages and development tools, and to support a wide range of both process- and artifact-oriented based validation techniques.