A verified model checker for the modal -calculus in Coq Export

@inproceedings{citeulike:3855559, abstract = {Abstract. We report on the formalisation and correctness proof of a model checker for the modal-calculus in Coq\&\#039;s constructive type theory. Using Coq\&\#039;s extraction mechanism we obtain an executable Caml program, which is added as a safe decision procedure to the system. An example illustrates its application in combination with deduction. 1}, author = {Sprenger, Christoph}, booktitle = {In TACAS, volume 1384 of LNCS}, citeulike-article-id = {3855559}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.1486}, keywords = {agdaspin, model-checking, theorem-proving}, posted-at = {2009-01-07 01:38:23}, priority = {0}, title = {A verified model checker for the modal -calculus in Coq}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.1486}, year = {1998} }

TY - CONF ID - citeulike:3855559 L3 - citeulike-article-id:3855559 N2 - Abstract. We report on the formalisation and correctness proof of a model checker for the modal-calculus in Coq's constructive type theory. Using Coq's extraction mechanism we obtain an executable Caml program, which is added as a safe decision procedure to the system. An example illustrates its application in combination with deduction. 1 TI - A verified model checker for the modal -calculus in Coq T2 - In TACAS, volume 1384 of LNCS KW - agdaspin KW - model-checking KW - theorem-proving AU - Sprenger, Christoph PY - 1998/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.1486 ER -