Introduction
The goals of the Programatica project are to
- develop
methodologies, tools and foundations to support the construction
and certification of high-assurance systems.
- integrate
a broad and open spectrum of assurance techniques
(code review, testing, formal methods, ...)
- support
evolving code, evidence, and assurance requirements
(e.g., track dependencies, revalidate evidence, ...)
- apply
to assurance of security properties in complex software artifacts
of engineering significance.
The Programatica approach to achieving these goals is to
- build a program development environment that supports and
encourages its users in thinking about,
stating, and validating key
properties.
- enable programming and
validation to proceed
hand in hand, using properties to link the two.
- allow users to realize benefits gradually by
choosing between varying levels of assurance.
The key components used are
- a semantically rich, formal modeling and implementation
language (Haskell).
- an expressive programming logic that can be used to
capture critical program properties (P-logic).
[TODO: Link to a nice introduction to P-logic]
- a toolset for creating, maintaining, and auditing the
supporting evidence (pfe, cert, ...).
[TODO: say something about Osker and
House]