Abstract
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.
This research was supported in part by the grant SFU/PRG 06-3, and by the Swiss National Science Foundation.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Cerny, P., Gupta, G., Madhusudan, P.: Synthesis of interface specifications for Java classes. In: Proc. POPL, pp. 98–109. ACM Press, New York (2005)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75, 87–106 (1987)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proc. FSE, pp. 109–120. ACM Press, New York (2001)
Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: Proc. FSE, pp. 31–40. ACM Press, New York (2005)
Hopcroft, J.E.: An n·logn algorithm for minimizing states in a finite automaton. In: Proc. Theory of Machines and Computations, pp. 189–196. Acad. Press, San Diego (1971)
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103, 299–347 (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beyer, D., Henzinger, T.A., Singh, V. (2007). Algorithms for Interface Synthesis. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)