Kleene Algebra with Tests and Coq Tools for while Programs

被引：0
作者：
Pous, Damien [1 ]
机构：
[1] ENS Lyon, CNRS LIP, UMR 5668, Lyon, France
来源：
INTERACTIVE THEOREM PROVING, ITP 2013 | 2013年 / 7998卷
关键词：
REGULAR EXPRESSIONS; COMPLETENESS; DERIVATIVES;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a Coq library about Kleene algebra with tests, including a proof of their completeness over the appropriate notion of languages, a decision procedure for their equational theory, and tools for exploiting hypotheses of a certain kind in such a theory. Kleene algebra with tests make it possible to represent if-then-else statements and while loops in imperative programming languages. They were actually introduced as an alternative to propositional Hoare logic. We show how to exploit the corresponding Coq tools in the context of program verification by proving equivalences of while programs, correctness of some standard compiler optimisations, Hoare rules for partial correctness, and a particularly challenging equivalence of flowchart schemes.
引用
收藏
页码：180 / 196
页数：17
相关论文
共 31 条
  • [1] Allen S. F., 1990, Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science (90CH2897-7), P95, DOI 10.1109/LICS.1990.113737
  • [2] Almeida JB, 2011, LECT NOTES COMPUT SC, V6482, P59, DOI 10.1007/978-3-642-18098-9_7
  • [3] Angus A., 2001, TR20011844 CORN U CS
  • [4] Partial derivatives of regular expressions and finite automaton constructions
    Antimirov, V
    [J]. THEORETICAL COMPUTER SCIENCE, 1996, 155 (02) : 291 - 319
  • [5] Armstrong Alasdair, 2012, Relational and Algebraic Methods in Computer Science. Proceedings 13th International Conference, RAMiCS 2012, P66, DOI 10.1007/978-3-642-33314-9_5
  • [6] Asperti Andrea, 2012, Interactive Theorem Proving. Proceedings of the Third International Conference, ITP 2012, P283, DOI 10.1007/978-3-642-32347-8_19
  • [7] Bertot Y, 2008, LECT NOTES COMPUT SC, V5170, P86, DOI 10.1007/978-3-540-71067-7_11
  • [8] Boyer R.S., 1981, The Correctness Problem in Computer Science
  • [9] Braibant T, 2010, LECT NOTES COMPUT SC, V6172, P163, DOI 10.1007/978-3-642-14052-5_13
  • [10] DERIVATIVES OF REGULAR EXPRESSIONS
    BRZOZOWSKI, JA
    [J]. JOURNAL OF THE ACM, 1964, 11 (04) : 481 - &
1234