\begin{titlepage}
\renewcommand{\thepage}{Title}
\vspace*{0.9in}
\begin{center}
{\LARGE Roadmap for Enhanced Languages and Methods \\ to Aid Verification} \\
~ \\
Gary T. Leavens, Jean-Raymond Abrial, Don Batory, Michael Butler,
Alessandro Coglio, Kathi Fisler, Eric Hehner, Cliff Jones,
Dale Miller, Simon Peyton-Jones, Murali Sitaraman, Douglas R. Smith,
and Aaron Stump \\
 ~ \\
TR \#06-21 \\
July 2006
\end{center}

\thispagestyle{empty}

\vfill

{\bf Keywords:}  Verification, verified software grand challenge,
specification languages, program generation,
correctness by construction, programming languages, tools,
annotations.

{\bf 2006 CR Categories:}

\noindent
D.2.1 [{\em Software Engineering\/}]
        Requirements/Specifications --- languages, methodologies;
D.2.2 [{\em Software Engineering\/}]
        Design Tools and Techniques --- modules and interfaces,
        object-oriented design methods;
D.2.4 [{\em Software Engineering\/}]
        Software/Program Verification --- assertion checkers, class
        invariants, correctness proofs, formal methods, model
        checking, programming by contract;
D.2.5 [{\em Software Engineering\/}]
        Testing and Debugging --- debugging aids, symbolic execution;
D.2.6 [{\em Software Engineering\/}]
        Programming Environments --- integrated environments;
D.2.7 [{\em Software Engineering\/}]
        Distribution, Maintenance, and Enhancement --- documentation;
D.2.10 [{\em Software Engineering\/}]
        Design -- methodologies, representation;
D.2.11 [{\em Software Engineering\/}]
        Software Architecture --- data abstraction, 
        information hiding, languages;
D.2.12 [{\em Software Engineering\/}]
        Reusable Software --- reusable libraries;
D.3.1 [{\em Programming Languages\/}]
	Formal Definitions and Theory --- semantics;
D.3.2 [{\em Programming Languages\/}]
        Language Classifications --- extensible languages, 
        specialized application languages, very high-level languages;
D.3.3 [{\em Programming Languages\/}]
	Language Constructs and Features --- abstract data types,
        classes and objects;
D.3.4 [{\em Programming Languages\/}]
        Processors --- translator writing systems and compiler generators;
F.3.1 [{\em Logics and Meanings of Programs\/}]
        Specifying and Verifying and Reasoning about Programs ---
        assertions, invariants, logics of programs, mechanical
        verification, pre- and post-conditions, specification techniques;
F.3.2 [{\em Logics and Meanings of Programs\/}]
        Semantics of Programming Languages --- program analysis;
F.3.3 [{\em Logics and Meanings of Programs\/}]
        Studies of Program Constructs --- control primitives,
        functional constructs, object-oriented constructs, type structure.

Submitted for publication.

Copyright {\copyright} 2006 by the authors.

\vspace*{0.2in}

\begin{center}
Department of Computer Science \\
226 Atanasoff Hall \\
Iowa State University \\
Ames, Iowa 50011-1041, USA
\end{center}
\end{titlepage}

\newpage
\setcounter{page}{1}