Advertisement

Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic

  • Yoshifumi Yuasa
  • Yoshinori Tanabe
  • Toshifusa Sekizawa
  • Koichi Takahashi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)

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.

Keywords

Pointer Structure Validity Checker Kripke Structure Proof Assistant Modal Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Agda Official Home Page, http://unit.aist.go.jp/cvs/Agda/
  2. 2.
    Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 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
  4. 4.
    Hubert, T., Marché, C.: A case study of C source code verification: the Schorr-Waite algorithm. In: Proc. Software Engineering and Formal Methods (SEFM 2005), pp. 190–199. IEEE Computer Society, Los Alamitos (2005)CrossRefGoogle Scholar
  5. 5.
    Loginov, A., Reps, T.W., Sagiv, M.: Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 261–279. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 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
  7. 7.
    Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)CrossRefGoogle Scholar
  8. 8.
    Schorr, H., Waite, W.M.: An efficient machine-independent procedure for garbage collection in various list structures. Commun. ACM 10(8), 501–506 (1967)zbMATHCrossRefGoogle Scholar
  9. 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. 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. 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. 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
  13. 13.
    Zappe, J.: Modal μ-calculus and alternating tree automata. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 171–184. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Yoshifumi Yuasa
    • 1
    • 4
  • Yoshinori Tanabe
    • 2
    • 4
  • Toshifusa Sekizawa
    • 3
    • 4
  • Koichi Takahashi
    • 4
  1. 1.Graduate School of Information Science and EngineeringTokyo Institute of Technology 
  2. 2.Graduate School of Information Science and TechnologyUniversity of Tokyo 
  3. 3.Graduate School of Information Science and TechnologyOsaka University 
  4. 4.Research Center for Verification and Semantics (CVS)National Institute of Advanced Industrial Science and Technology (AIST) 

Personalised recommendations