RSRG: Benchmarks


Early Benchmarks for Verification

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]

  1. Adding and Multiplying Numbers

    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.

  2. Binary Search in an Array

    Problem Requirements: Verify an operation that uses binary search to find a given entry in an array of entries that are in sorted order.

  3. Reversing a Queue

    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.)

  4. Sorting a Queue

    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.

  5. Layered Implementation of a Map ADT

    Problem Requirements: Verify an implementation of a generic map ADT, where the data representation is layered on other built-in types and/or ADTs.

  6. Linked-List Implementation of a Queue ADT

    Problem Requirements: Verify an implementation of the queue type specified for an earlier benchmark, using a linked data structure for the representation.

  7. Iterators

    Problem Requirements: Verify a client program that uses an iterator for some collection type, as well as an implementation of the iterator.

  8. Input/Output Streams

    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.

  9. An Integrated Application

    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.


Bruce W. Weide
Last modified: Sun Nov 16 18:08:06 EST 2008