1 Implementing a Model Checker for LEGO Export

@misc{citeulike:3816365, abstract = {Abstract. Interactive theorem proving provides a general approach to modelling and verification of both hardware and software systems but requires significant human efforts to deal with many tedious proofs. To be effectively used in practice, we need some automatic tools such as model checkers to deal with those tedious proofs. In this paper, we formalise a verification system of both CCS and an imperative language in the proof development system LEGO which can be used to verify both finite and infinite problems. Then a model checker, LegoMC, is implemented to generate LEGO proof terms for finite-state problems automatically. Therefore people can use LEGO to verify a general problem with some of its finite sub-problems verified by LegoMC. On the other hand, this integration extends the power of model checking to verify more complicated and infinite models as well. 1}, author = {Yu, Shenwei and Luo, Zhaohui}, citeulike-article-id = {3816365}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.355}, keywords = {agdaspin, copy, model-checking, print, theorem-proving}, posted-at = {2008-12-22 02:35:47}, priority = {0}, title = {1 Implementing a Model Checker for LEGO}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.355} }

TY - ELEC ID - citeulike:3816365 L3 - citeulike-article-id:3816365 N2 - Abstract. Interactive theorem proving provides a general approach to modelling and verification of both hardware and software systems but requires significant human efforts to deal with many tedious proofs. To be effectively used in practice, we need some automatic tools such as model checkers to deal with those tedious proofs. In this paper, we formalise a verification system of both CCS and an imperative language in the proof development system LEGO which can be used to verify both finite and infinite problems. Then a model checker, LegoMC, is implemented to generate LEGO proof terms for finite-state problems automatically. Therefore people can use LEGO to verify a general problem with some of its finite sub-problems verified by LegoMC. On the other hand, this integration extends the power of model checking to verify more complicated and infinite models as well. 1 TI - 1 Implementing a Model Checker for LEGO KW - agdaspin KW - copy KW - model-checking KW - print KW - theorem-proving AU - Yu, Shenwei AU - Luo, Zhaohui UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.355 ER -