Skip to main content
SpringerLink
Log in

Temporal Verification of Programs via First-Order Fixpoint Logic

  • Conference paper
  • First Online:
Static Analysis (SAS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11822))

Included in the following conference series:

Abstract

This paper presents a novel program verification method based on Mu-Arithmetic, a first-order logic with integer arithmetic and predicate-level least/greatest fixpoints. We first show that linear-time temporal property verification of first-order recursive programs can be reduced to the validity checking of a Mu-Arithmetic formula. We also propose a method for checking the validity of Mu-Arithmetic formulas. The method generalizes a reduction from termination verification to safety property verification and reduces validity of a Mu-Arithmetic formula to satisfiability of CHC, which can then be solved by using off-the-shelf CHC solvers. We have implemented an automated prover for Mu-Arithmetic based on the proposed method. By combining the automated prover with a known reduction and the reduction from first-order recursive programs above, we obtain: (i) for while-programs, an automated verification method for arbitrary properties expressible in the modal \(\mu \)-calculus, and (ii) for first-order recursive programs, an automated verification method for arbitrary linear-time properties expressible using Büchi automata. We have applied our Mu-Arithmetic prover to formulas obtained from various verification problems and obtained promising experimental results.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We remark that, for those who are familiar with fixpoint logics, \(P_2(x)\) can be written as \(\nu P_2.\lambda x.P_2(x+1)\wedge (\mu P_1.\lambda y.y= x\vee P_1(y+1))\,0\) in the ordinary syntax of Mu-Arithmetic [11] or HFL [40].

  2. 2.

    The assumption on non-termination is guaranteed by renaming \(\mathbf {main}\) to \(\mathbf {main}'\), and adding the function definitions \(\mathbf {main}() = \mathbf {let}\ x=\mathbf {main}'()\ \mathbf {in}\ { loop ()}\) and \( loop ()=A_{ call };{ loop }{}\); the last assumption is guaranteed by restricting the righthand side of each function definition to an expression of the form \(A_{ call };{e}\).

  3. 3.

    https://github.com/hkhlaaf/T2/blob/master/test/ctlstar_test.t2.

  4. 4.

    There are some discrepancies on the verification results among [3, 17] and ours. We are not sure about this, but it is most likely because the benchmark set has accidentally been modified when it was passed around. We have taken the industrial set from that of E-HSF [3] provided by Andrey Rybalchenko. Note, however, that we found some discrepancies between the C programs and their encodings in the E-HSF; that explains the difference between the outputs of our tool and those of E-HSF [3]. The “small” set was provided by Eric Koskinen. For 26–28, the results are “invalid” for both \(\varphi \) and \(\lnot \varphi \) (as in [3]); this is not a contradiction, as the checked properties are of the form “for all the initial states, \(\varphi \) (or \(\lnot \varphi \)) holds.”.

References

  1. Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Program. Lang. Syst. 27(4), 786–818 (2005)

    Article  Google Scholar 

  2. Andersen, H.R.: Model checking and boolean graphs. Theor. Comput. Sci. 126(1), 3–30 (1994)

    Article  Google Scholar 

  3. Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869–882. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_61

    Chapter  Google Scholar 

  4. Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci. 66(2), 160–177 (2002)

    Article  Google Scholar 

  5. Bjørner, N., Gurfinkel, A.: Property directed polyhedral abstraction. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 263–281. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46081-8_15

    Chapter  Google Scholar 

  6. Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23534-9_2

    Chapter  Google Scholar 

  7. Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_8

    Chapter  Google Scholar 

  8. Bjørner, N., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, pp. 3–11. EasyChair (2012)

    Google Scholar 

  9. Bjørner, N., McMillan, K.L., Rybalchenko, A.: Higher-order program verification as satisfiability modulo theories with algebraic data-types. CoRR abs/1306.5264 (2013)

    Google Scholar 

  10. Blass, A., Gurevich, Y.: Existential fixed-point logic. In: Börger, E. (ed.) Computation Theory and Logic. LNCS, vol. 270, pp. 20–36. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-18170-9_151

    Chapter  Google Scholar 

  11. Bradfield, J.C.: Fixpoint alternation and the game quantifier. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 350–361. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48168-0_25

    Chapter  Google Scholar 

  12. Burn, T.C., Ong, C.L., Ramsay, S.J.: Higher-order constrained horn clauses for verification. PACMPL 2(POPL), 11:1–11:28 (2018)

    Google Scholar 

  13. Champion, A., Chiba, T., Kobayashi, N., Sato, R.: ICE-based refinement type discovery for higher-order functional programs. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 365–384. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_20

    Chapter  Google Scholar 

  14. Cook, B., Khlaaf, H., Piterman, N.: Fairness for infinite-state systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 384–398. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_30

    Chapter  MATH  Google Scholar 

  15. Cook, B., Khlaaf, H., Piterman, N.: Verifying increasingly expressive temporal logics for infinite-state systems. J. ACM 64(2), 15:1–15:39 (2017)

    Article  MathSciNet  Google Scholar 

  16. Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: POPL 2011, pp. 399–410. ACM (2011)

    Google Scholar 

  17. Cook, B., Koskinen, E.: Reasoning about nondeterminism in programs. In: PLDI 2013, pp. 219–230. ACM (2013)

    Google Scholar 

  18. Cook, B., Koskinen, E., Vardi, M.: Temporal property verification as a program analysis task. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 333–348. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_26

    Chapter  Google Scholar 

  19. Delzanno, G., Podelski, A.: Constraint-based deductive model checking. STTT 3(3), 250–270 (2001)

    MATH  Google Scholar 

  20. Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 49–66. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_4

    Chapter  Google Scholar 

  21. Fedyukovich, G., Zhang, Y., Gupta, A.: Syntax-guided termination analysis. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 124–143. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_7

    Chapter  Google Scholar 

  22. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of PLDI 2012, pp. 405–416 (2012)

    Article  Google Scholar 

  23. Hofmann, M., Chen, W.: Abstract interpretation from Büchi automata. In: CSL-LICS 2014, pp. 51:1–51:10. ACM (2014)

    Google Scholar 

  24. Jaffar, J., Santosa, A.E., Voicu, R.: A CLP method for compositional and intermittent predicate abstraction. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 17–32. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_2

    Chapter  MATH  Google Scholar 

  25. Kobayashi, N., Lozes, É., Bruse, F.: On the relationship between higher-order recursion schemes and higher-order fixpoint logic. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017, pp. 246–259. ACM (2017)

    Google Scholar 

  26. Kobayashi, N., Tsukada, T., Watanabe, K.: Higher-order program verification via HFL model checking. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 711–738. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_25

    Chapter  Google Scholar 

  27. Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17–34. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_2

    Chapter  Google Scholar 

  28. Koskinen, E., Terauchi, T.: Local temporal reasoning. In: CSL-LICS 2014. pp. 59:1–59:10. ACM (2014)

    Google Scholar 

  29. Lozes, É.: A type-directed negation elimination. In: Matthes, R., Mio, M. (eds.) Proceedings Tenth International Workshop on Fixed Points in Computer Science, FICS 2015, Berlin, Germany, September 11–12, 2015. EPTCS, vol. 191, pp. 132–142 (2015)

    Article  MathSciNet  Google Scholar 

  30. Lubarsky, R.S.: \(\mu \)-definable sets of integers. J. Symbolic Logic 58(1), 291–313 (1993)

    Article  MathSciNet  Google Scholar 

  31. Murase, A., Terauchi, T., Kobayashi, N., Sato, R., Unno, H.: Temporal verification of higher-order functional programs. In: Proceedings of POPL 2016 (2016, to appear)

    Google Scholar 

  32. Nanjo, Y., Unno, H., Koskinen, E., Terauchi, T.: A fixpoint logic and dependent effects for temporal property verification. In: LICS 2018, pp. 759–768. ACM, July 2018

    Google Scholar 

  33. Kobayashi, N., Nishikawa, T., A.I., Unno, H.: Temporal verification of programs via first-order fixpoint logic. A longer version, available from the first author’s web page (2019)

    Google Scholar 

  34. Peralta, J.C., Gallagher, J.P., Sağlam, H.: Analysis of imperative programs through analysis of constraint logic programs. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 246–261. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49727-7_15

    Chapter  Google Scholar 

  35. Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004, pp. 32–41. IEEE (2004)

    Google Scholar 

  36. Podelski, A., Rybalchenko, A.: Transition invariants. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14–17 July 2004, Turku, Finland, Proceedings, pp. 32–41 (2004)

    Google Scholar 

  37. Seidl, H., Neumann, A.: On guarding nested fixpoints. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 484–498. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48168-0_34

    Chapter  Google Scholar 

  38. Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 571–591. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_30

    Chapter  Google Scholar 

  39. Urban, C., Ueltschi, S., Müller, P.: Abstract interpretation of CTL properties. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 402–422. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99725-4_24

    Chapter  Google Scholar 

  40. Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 512–528. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_33

    Chapter  Google Scholar 

  41. Watanabe, K., Tsukada, T., Oshikawa, H., Kobayashi, N.: Reduction from branching-time property verification of higher-order programs to HFL validity checking. In: PEPM 2019. ACM (2019)

    Google Scholar 

Download references

Acknowledgments

We would like to thank anonymous referees for useful comments. This work was supported by JSPS KAKENHI Grant Number JP15H05706 and JP16H05856.

Author information

Authors and Affiliations

  1. The University of Tokyo, Tokyo, Japan

    Naoki Kobayashi

  2. Kyoto University, Kyoto, Japan

    Takeshi Nishikawa & Atsushi Igarashi

  3. University of Tsukuba, Tsukuba, Japan

    Hiroshi Unno

  4. RIKEN AIP, Tokyo, Japan

    Hiroshi Unno

Authors
  1. Naoki Kobayashi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Takeshi Nishikawa
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Atsushi Igarashi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Hiroshi Unno
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Naoki Kobayashi .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, CO, USA

    Bor-Yuh Evan Chang

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kobayashi, N., Nishikawa, T., Igarashi, A., Unno, H. (2019). Temporal Verification of Programs via First-Order Fixpoint Logic. In: Chang, BY. (eds) Static Analysis. SAS 2019. Lecture Notes in Computer Science(), vol 11822. Springer, Cham. https://doi.org/10.1007/978-3-030-32304-2_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32304-2_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32303-5

  • Online ISBN: 978-3-030-32304-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation