We are currently documenting progress and results using the following early benchmarks along a path toward verified software: "one small step" at a time. For more information about these benchmarks, see:
Weide, B.W., Sitaraman, M., Harton, H.K., Adcock, B., Bucci, P., Bronish, D., Heym, W.D., Kirschenbaum, J., and Frazier, D., "Incremental Benchmarks for Software Verification Tools and Techniques", Proceedings of VSTTE 2008 (Verified Software: Theories, Tools, and Experiments), Springer-Verlag LNCS 5295, October 2008, 84-98. [PDF]
Problem Requirements: Verify an operation that adds two numbers by repeated incrementing. Verify an operation that multiplies two numbers by repeated addition, using the first operation to do the addition. Make one algorithm iterative, the other recursive.
Problem Requirements: Verify an operation that uses binary search to find a given entry in an array of entries that are in sorted order.
Problem Requirements: Specify a user-defined FIFO queue ADT. Verify two implementations (one iterative, one recursive) for an operation that reverses a queue. (Note: the iterative version may need to use another component, e.g., a LIFO stack ADT, in which case that also needs to be specified, of course.)
Problem Requirements: Specify a user-defined FIFO queue ADT that is generic (i.e., parameterized by the type of entries in a queue). Verify an operation that uses this component to sort the entries in a queue into some client-defined order.
Problem Requirements: Verify an implementation of a generic map ADT, where the data representation is layered on other built-in types and/or ADTs.
Problem Requirements: Verify an implementation of the queue type specified for an earlier benchmark, using a linked data structure for the representation.
Problem Requirements: Verify a client program that uses an iterator for some collection type, as well as an implementation of the iterator.
Problem Requirements: Specify simple input and output capabilities such as character input streams and output streams (with the flavor of C++ streams, for example). Verify an application program that uses them in conjunction with one of the components from the earlier benchmarks.
Problem Requirements: Verify an application program with a concisely stated set of requirements, where the particular solution relies on integration of at least a few of the previous benchmarks. For example, verify an application program that does the following: Given input containing a series (in arbitrary order) of terms and their definitions, output an HTML glossary that presents all the terms and their definitions, with (a) the terms in alphabetical order, and (b) a hyperlink from each term that occurs in any definition to that term's location in the glossary.