Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic
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.
KeywordsPointer Structure Validity Checker Kripke Structure Proof Assistant Modal Formula
Unable to display preview. Download preview PDF.
- 1.Agda Official Home Page, http://unit.aist.go.jp/cvs/Agda/
- 3.Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI International Cambridge Computer Science Research Center (1995)Google Scholar
- 6.Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 121–135. Springer, Heidelberg (2003)Google Scholar
- 9.Sekizawa, T., Tanabe, Y., Yuasa, Y., Takahashi, K.: MLAT: A tool for heap analysis based on predicate abstraction by modal logic. In: The IASTED International Conference on Software Engineering (SE 2008), pp. 310–317 (2008)Google Scholar
- 10.Tanabe, Y., Sekizawa, T., Yuasa, Y., Takahashi, K.: Pre- and post-conditions expressed in variants of the modal μ-calculus. CVS/AIST Research Report AIST-PS-2008-009, CVS/AIST (2008)Google Scholar
- 11.Tanabe, Y., Takahashi, K., Hagiya, M.: A decision procedure for alternation-free modal μ-calculi. In: Advances in Modal Logic (to appear, 2008)Google Scholar
- 12.Yang, H.: An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In: Proceedings of the 1st Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (2001)Google Scholar