Abstract
Verification is a hard task, but much progress has been achieved recently. Many verification problems have been shown decidable by reducing them to model-checking finite state transition systems. Verification of infinite state transition systems has achieved tremendous progress too, by showing that many particular cases were themselves decidable, such as timed automata [1] or some forms of pushdown-automata [4]. However, the demand for verification is growing fast, and the industrial needs go far beyond the verification of decidable systems.
This work was partly supported by the RNTL project AVERROES.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. To appear in Mathematical Structures in Computer Science ( 2003)
Blanqui, F., Jouannaud, J.P., Strub, P.Y.: A calculus of congruent construction. Check web for updates (2004)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Chrzaszcz, J.: Modules in Coq Are and Will Be Correct. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 130–146. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jouannaud, JP. (2004). Theorem Proving Languages for Verification. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive