Outline of Theory Challenges

Outline of theory challenges

This page organizes challenges and milestones promulgated by the Theory panel into the new VS roadmap research categories. These are intended to be integrated into the VS roadmap under the major research headings, as brief items with links to elaboration text.

Challenges and milestones (with time frame) are both included here; major milestons will be excerpted in the executive summary of the roadmap. Composition is a crosscutting theme; in a sense it is the challenge; it should appear in many forms in the different research categories.

Modeling of requirements (specification methods)

This area includes the design of domain models and ground (golden) models for requirements elicitation and capture. See Boerger's paper

• concepts for decomposition and modularization, including crosscutting concerns, integration of views meaningful to different stakeholders or at different levels of detail; requirements database
• specifying security properties
• specifying intensional properties (e.g., time and space complexity of lazy functional programs)
• integrating disparate models of computation in hybrid systems (discrete event; continuous time; synchronous dataflow; etc)

Design methods

• refinement of abstract models (cf. CxC panel roadmap)
• Program generation and staging

  Programmer-controlled generation of program code and other documents. This topic has relations to correctness of code generation and compilation; but whereas a lot of one-time effort can (and should) be invested in proving a compiler correct, this section is about improving the reliability ad hoc generators. Thousands of such generators are written by practitioners, to generate J2EE deployment descriptors and interfaces, web pages, Javascript functions, various forms of glue code, SQL statements and so on. Also, such generators are essential to realize model driven development. Type theories are needed to support checking of multistage programs. For detailed challenges, see Sestoft's Correctness of Multistage Notations.

Verification methods

This area focuses on verification of software/designs in general; verification of tools falls under Integrated Verification Environments.

• proof techniques including techniques for proving the correctness of refinements. We emphasize the last refinement step, to executable code; absent adequate code generators, the last step of a formal development is often an informal translation to code.
• software model checking and data flow analysis using abstract interpretation
• Develop a systematic and useful theory of practical precision_ and _practical running time of automatic analysis/verification methods.

  Empirical observations show that certain automatic verification methods with bad worst case-complexity and/or imperfect precision work well for typical practical problems. A "systematic and useful theory" should explain this and also allow to predict the practical behavior by theoretical means. Such an explanation could be of great practical importance, as it could direct research towards practical methods. The current state-of-the-art in this area is rather of a trial-and-error kind where analysis procedures are tuned on the basis of benchmark examples.

• logics, including semantics; challenges remain even for Imperative Program Logics
• concurrency Concurrency
• certifying compilation: translation of source-level proofs/specifications to lower level code; this is especially difficult in case of low level compiler optimizations and properties beyond memory safety. For details see Compiler Verification by Leroy, Mueller-Olm and Boerger, and the List Machine benchmark challenge
• type systems (specification and modular, automatic checking of lightweight properties) For more details, see Zdancewic's s Type Systems
• language subsets and features (associated proof techniques)

  A long term challenge is for a theory that gives separate accounts for individual notations, so that development and analysis of a system component can be carried out not in terms of a fixed "language", a subset of which is used in the component, but rather a selection of notations needed for that component. The theory should account for reasoning principles associated with these notations and in particular guide the composition of sound tools no more complex than necessary for the particular selection of notations.

Integrated verification environments

• interoperable tools
• Linking theories as unifying foundation for tool integration (e.g., linking theory for sound embedding ACL2 and HOL). See Hoare's Goals of Unifying Theories and Woodcock's [[Current Research on Unifying Theories]]?.
• Translating verification problems (e.g., refinement reduced to safety)
• verification of the tools
  • translation validation (e.g., Pnueli/Zuck): verify the outcome of single compiler run, i.e., that target program is correct in some sense with respect to the source program. Compiler could additionally generate a certificate to aid the verifier.
  • compiler verification See Compiler Verification details by Leroy, Mueller-Olm, and Boerger.
  • verification of type checkers and inferencers (cf. the POPLmark challenge and Type systems)
  • verification of secure flow checker (integrating type checking and assertion-based verification) See Secure Flow Checking