Efficient reasoning about executable specifications in Coq. (English) Zbl 1013.68539
Carreño, Victor A. (ed.) et al., Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2410, 31-46 (2002).
Summary: We describe a package to reason efficiently about executable specifications in Coq. The package provides a command for synthesizing a customized induction principle for a recursively defined function, and a tactic that combines the application of the customized induction principle with automatic rewriting. We further illustrate how the package leads to a drastic reduction (by a factor of 10 approximately) of the size of the proofs in a large-scale case study on reasoning about JavaCard.
For the entire collection see [Zbl 0997.00025].
For the entire collection see [Zbl 0997.00025].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
