Testing And Proving Distributed Algorithms In Constructive Type Theory
TAP'07: Proceedings of the 1st international conference on Tests and proofs（2007）
摘要
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.
更多查看译文
关键词
deadlock property,liveness property,constructive type theory,dependent type,expensive proof effort,functional programming language
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要