Theory roadmap outline

SUPERSEDED BY Working Outline

Introduction

This report outlines a road map for research in the semantics and axiomatics of notations for programs, designs, specifications, and requirements models. This report has been written by Theory Panel with the following membership: Egon Boerger, Xavier Leroy, Markus Mueller-Olm, David Naumann, Peter O'Hearn, John Reynolds, Peter Sestoft and Steve Zdancewic.

Goals of the Panel

• To create a road map that identifies research challenges in the theory of program construction and analysis that are critical for the overall goals of the verification grand challenge.
• To interact with the other Verified Software panels in order to refine these challenges as increasingly specific goals and activities emerge.
• Coordinating the activities of researchers who seek to meet those challenges.
• Generating publicity to broaden the participation in the effort.

Theoreticians will benefit from VSR through interaction with experimenters. We will get evidence that our methods for system definition and validation (simulators, checkers and proof systems) are or are not usable for programs of practical interest. If a validation or verification attempt fails apparently due to limitations of a simulator or checker or proof system, this may pose a substantial new challenge for theory, or alternatively an opportunity for an existing theory to be better explained and fully embodied in tools. (We'll find out which ``straightforward generalizations'' are actually so.)

The goals listed are very high level. The primary topic of the initial discussions of this panel has been the absence of sufficient focus. Without sharply focused goals for the Verified Software project, a very wide range of theory can be considered pertinent. Predictably, the current report reflects a range narrowed mainly by the interests of the current active panel members. At the same time it reflects our attempts to supply the missing focus for the initiative as a whole.

DN: in my opinion it is imperative that the overarching roadmap designate a small number of target computer systems as having high priority, with milestones in each five-year period. The milestones will encompass ground modeling, refinement, as well as verification with respect to detailed formal specifications of deep and shallow properties. Such focus would leave plenty of room for various groups to participate and carry out activities as they choose. But more importantly it would provide focus for the process of formulating, discussing, and prioritizing milestones and activities for those who see the VSR challenge as an opportunity for more closely coordinating theoretical research with its application.

Focus of panel:

• Semantics and logics of "realistic" programming and modeling languages used in experiments
• Correctness of compilers, compilation schemes, and program analysis tools
• Correctness of refinement and analysis tools for models? or this falls under the purview of correct-by-construction panel
• Semantics for multi-stage notations (meta-programming, program generation, scripting for tool interoperation,...)
• Linking theories, as unifying foundation for integration of disparate tools

Background on theory for verified software

Theory is needed to support the following.

• Construction and analysis of ``ground models'', i.e. abstract rigorous system blueprints, to correctly and completely capture and document system requirements as starting point (contract) for further design leading to code.
• Derivation of one system description from another, e.g. definition of a refinement of an abstract system model, and proving the desired correctness properties (e.g. equivalence or preservation of behavioral properties), either in the meta-theory ("correctness by construction") or as post hoc mathematical verification or experimental validation of a particular refinement step.
• Composition and modularization techniques, together with corresponding proof principles, needed to support the analysis of run-time features.

These items encompass design validation, ordinary program correctness (e.g., correctness of a particular C program with respect to a given spec), and meta-theory (e.g., soundness of a proof rule or transformation and correctness of a compiler with respect to a language and a processor semantics). Theory provides the semantics that underlies notations that express system requirements, design specifications, and implementations. It provides definitions for notions such as satisfaction and refinement. It provides general laws and other theorems that justify methods for reasoning about particular specifications, designs, and implementations. Theory includes meta-theory, i.e., general definitions concerning other theories: e.g., a notion of retraction between process algebras, or the soundness of a Hoare logic for a particular assertion language and programming language, or a verification condition generator (VCG) embodying a semantics of specifications and of programs where the theory encompasses these semantics and also their justification in terms of alternative semantics that may be closer to the actual machine.

Generally speaking, theory has to provide methods for linking in a verifiable way the application-centric meaning of a system, which is expressed by a ground model prior to coding, to the meaning of the implementing code that is verified by the compiler. In particular, theory has to define provably correct refinement schemes that support further detailing of abstract specifications to their implementation by compilable code (read: the design process leading from system requirements to executable code).

Current state of theory

CS Theory started in the first third of the 20-th century with computability theory, whose main discovery was Turing's notion of a programmable universal computing machine. With the advent of computers CS Theory quickly focussed

• on the hardware side on the theory of circuits and computer architectures,
• on the software side on the theory of algorithms, data structures and programming languages.

Numerous theoretical achievements in these fields are nowadays incorporated into advanced tools for the design and the analysis of modern programming languages and compilable programs. This includes powerful static and dynamic analysis techniques, e.g. type inference engines, mechanical verification of type correctness and similar program properties, etc.

With the growing complexity and diversity of computer-based systems one more abstraction level came into view, where prior to coding a system has to be specified by an abstract model to capture the system requirements in a faithful and complete manner, which can be used as starting point for its implementation by executable code. CS Theory has provided a large variety of such specification languages. Some of them come with tools supporting the development of abstract system models and their refinements to code.

Theory challenges

Open problems, research areas, and challenge problems are enumerated in a separate page: [Theory Challenges].

Planning and roadmap

Which challenge problems should be addressed first? In which time frames (1-5, 5-10, 10-15 years)?

Who are the researchers/groups interested?

What concrete activities are to be taken to address the challenges and how will these activities be integrated with the other verified software activities?