Abstract
One of the most significant developments in the area of design verification over the last decade is the development of of algorithmic methods for verifying temporal specification of finite-state designs [2]. A frequent criticism against this approach, however, is that verification is done after significant resources have already been invested in the development of the design. Since designs invariably contains errors, verification simply becomes part of the debugging process. The critics argue that the desired goal ought to be the use of the specification in the design development process in order to guarantee the development of correct designs. This is called design synthesis [1,4]. In this talk I will review 50 years of research on the synthesis problem and show how the automata-theoretic approach can be used to solve it [3,4,5].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Church, A.: Applicaton of recursive arithmetics to the problem of circuit synthesis. In: Summaries of Talks Presented at The Summer Institute for Symbolic Logic, Communications Research Division, Institute for Defense Analysis, pp. 3–50 (1957)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp. 531–540 (2005)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 179–190 (1989)
Rabin, M.O.: Automata on infinite objects and Church’s problem. Amer. Mathematical Society (1972)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vardi, M.Y. (2008). From Verification to Synthesis. In: Shankar, N., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2008. Lecture Notes in Computer Science, vol 5295. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87873-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-87873-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87872-8
Online ISBN: 978-3-540-87873-5
eBook Packages: Computer ScienceComputer Science (R0)