Testing and proving distributed algorithms in constructive type theory

被引：0
|
作者：
Haiyan, Qiao [1 ]
机构：
[1] Sun Yat Sen Univ, Dept Comp Sci, Guangzhou 510275, Peoples R China
来源：
TESTS AND PROOFS | 2007年 / 4454卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We report our experiences to verify distributed algorithms in constructive type theory by testing and proving. Properties can be tested to eliminate bugs before proving, thus saving expensive proof effort. Both deadlock property and liveness property are proven after testing. The verified algorithm can be executed in Cayenne, a functional programming language with dependent types.
引用
收藏
页码：79 / 94
页数：16
相关论文
共 50 条
  • [1] Combining testing and proving in dependent type theory
    Dybjer, P
    Haiyan, Q
    Takeyama, M
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2003, 2758 : 188 - 203
  • [2] PROVING GEOMETRY STATEMENTS OF CONSTRUCTIVE TYPE
    CHOU, SC
    GAO, XS
    LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 607 : 20 - 34
  • [3] Modeling and Proving Distributed Algorithms for Dynamic Graphs
    Fakhfakh, Faten
    Tounsi, Mohamed
    Mosbah, Mohamed
    FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2020, 108 : 751 - 761
  • [4] Algorithms for generating, testing and proving primes: A survey
    Mihailescu, P
    CRYPTOGRAPHY AND COMPUTATIONAL NUMBER THEORY, 2001, 20 : 93 - 122
  • [5] Theorem proving for constructive λ-calculus
    Ramsay, A
    ARTIFICIAL INTELLIGENCE: METHODOLOGY, SYSTEMS, APPLICATIONS, PROCEEDINGS, 2000, 1904 : 69 - 79
  • [6] APPROACH TO THEOREM PROVING IN TYPE THEORY
    ANDREWS, PB
    COHEN, EL
    JOURNAL OF SYMBOLIC LOGIC, 1979, 44 (03) : 477 - 478
  • [7] Proving and Disproving Information Inequalities: Theory and Scalable Algorithms
    Ho, Siu-Wai
    Ling, Lin
    Tan, Chee Wei
    Yeung, Raymond W.
    IEEE TRANSACTIONS ON INFORMATION THEORY, 2020, 66 (09) : 5522 - 5536
  • [8] Inaccessibility in constructive set theory and type theory
    Rathjen, M
    Griffor, ER
    Palmgren, E
    ANNALS OF PURE AND APPLIED LOGIC, 1998, 94 (1-3) : 181 - 200
  • [9] A Refinement-Based Approach for Proving Distributed Algorithms on Evolving Graphs
    Fakhfakh, Faten
    Tounsi, Mohamed
    Kacem, Ahmed Hadj
    Mosbah, Mohamed
    2016 IEEE 25TH INTERNATIONAL CONFERENCE ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE), 2016, : 44 - 49
  • [10] REFLECTIVE SEMANTICS OF CONSTRUCTIVE TYPE THEORY
    SMITH, SF
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 613 : 33 - 45
12345