The goals of the Programatica project were to
methodologies, tools and foundations to support the construction
and certification of high-assurance systems.
a broad and open spectrum of assurance techniques
(code review, testing, formal methods, ...)
evolving code, evidence, and assurance requirements
(e.g., track dependencies, revalidate evidence, ...)
to assurance of security properties in complex software artifacts
of engineering significance.
The Programatica approach to achieving these goals was to
- build a program development environment that supports and
encourages its users in thinking about,
stating, and validating key
- 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 were
- a semantically rich, formal modeling and implementation
- 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