Name
Abstract | ||
|---|---|---|
We have proposed an abstraction technique that uses the formulas of variants of the modal μ-calculus as a method for analyzing pointer manipulating programs. In this paper, the method is applied to verify the correctness of the Deutsch-Schorr-Waite marking algorithm, which is regarded as a benchmark of such analysis. Both the partial correctness and the termination are discussed. For the former, we built a system on top of the proof assistant Agda, with which the user constructs Hoare-style proofs. The system is an optimum combination of automatic and interactive approaches. While a decision procedure for a variant of modal μ-calculus, which is available through the Agda plug-in interface, enables the user to construct concise proofs, the run time is much shorter than for automatic approaches. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-87873-5_12 | VSTTE |
Keywords | Field | DocType |
proof assistant agda,concise proof,decision procedure,modal logic,interactive approach,optimum combination,agda plug-in interface,hoare-style proof,deutsch-schorr-waite marking algorithm,partial correctness,abstraction technique,automatic approach,proof assistant | Kripke structure,Pointer (computer programming),Programming language,Computer science,Correctness,Algorithm,Theoretical computer science,Mathematical proof,Modal logic,Agda,Modal,Proof assistant | Conference |
Volume | ISSN | Citations |
5295 | 0302-9743 | 1 |
PageRank | References | Authors |
0.35 | 6 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yoshifumi Yuasa | 1 | 2 | 1.05 |
| Yoshinori Tanabe | 2 | 124 | 13.96 |
| Toshifusa Sekizawa | 3 | 3 | 3.78 |
| Koichi Takahashi | 4 | 38 | 6.30 |