## Algorithms for Interface Synthesis

*Dirk Beyer,
Thomas A. Henzinger,
and Vasu Singh*

A temporal interface for a software component is a finite automaton
that specifies the legal sequences of calls to functions that are
provided by the component. We compare and evaluate three different
algorithms for automatically extracting temporal interfaces from
program code: (1) a *game* algorithm that computes the interface
as a representation of the most general environment strategy to avoid
a safety violation; (2) a *learning* algorithm that repeatedly
queries the program to construct the minimal interface automaton; and
(3) a *CEGAR* algorithm that iteratively refines an abstract
interface hypothesis by adding relevant program variables. For
comparison purposes, we present and implement the three algorithms in
a unifying formal setting. While the three algorithms compute the
same output and have similar worst-case complexities, their actual
running times may differ considerably for a given input program. On
the theoretical side, we provide for each of the three algorithms a
family of input programs on which that algorithm outperforms the two
alternatives. On the practical side, we evaluate the three algorithms
experimentally on a variety of Java libraries.

*Proceedings of the
19th International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 4590,
Springer, 2007, pp. 4-19.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2007 Springer.