Abstract
Higher-order model checking, or model checking of higher-order recursion schemes, has been recently applied to fully automated verification of functional programs. The previous approach has been indirect, in the sense that higher-order functional programs are first abstracted to (call-by-value) higher-order Boolean programs, and then further translated to higher-order recursion schemes (which are essentially call-by-name programs) and model checked. These multi-step transformations caused a number of problems such as code explosion. In this paper, we advocate a more direct approach, where higher-order Boolean programs are directly model checked, without transformation to higher-order recursion schemes. To this end, we develop a model checking algorithm for higher-order call-by-value Boolean programs, and prove its correctness. According to experiments, our prototype implementation outperforms the indirect method for large instances.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Note that the terms like \(\mathbf {assume}\ \mathbf {false}; t\) and \(\varOmega \) are not error expressions. They are intended to model divergent terms, although they are treated as stuck terms in the operational semantics for a technical convenience.
- 2.
In the call-by-name case, this property immediately follows from the condition
because \(t_2\) is not evaluated before the function call. - 3.
Unfortunately, we could not measure the elapsed time of HorSat2 for some large instances because it raised stack-overflow exceptions.
because References
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24756-2_1
Ball, T., Rajamani, S.K.: Bebop: a path-sensitive interprocedural dataflow engine. In: Proceedings of PASTE 2001, pp. 97–103. ACM (2001)
Broadbent, C.H., Carayol, A., Hague, M., Serre, O.: C-SHORe: acollapsible approach to higher-order verification. In: Proceedings of ICFP 2013, pp. 13–24 (2013)
Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Proceedings of CSL 2013, LIPIcs, vol. 23, pp. 129–148 (2013)
Gilray, T., Lyde, S., Adams, M.D., Might, M., Horn, D.V.: Pushdown control-flow analysis for free. In: Proceedings of POPL 2016, pp. 691–704. ACM (2016)
Horn, D.V., Might, M.: Abstracting abstract machines. In: Proceedings of ICFP 2010, pp. 51–62. ACM (2010)
Johnson, J.I., Horn, D.V.: Abstracting abstract control. In: Proceedings of DLS 2014, pp. 11–22. ACM (2014)
Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009, pp. 25–36. ACM (2009)
Kobayashi, N.: Model checking higher-order programs. J. ACM 60(3) (2013)
Kobayashi, N.: HorSat2: a saturation-based higher-order model checker. A toolpaper under submission (2015). http://www-kb.is.s.u-tokyo.ac.jp/~koba/horsat2
Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI 2011, pp. 222–233. ACM (2011)
Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 392–411. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54833-8_21
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)
Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS 2006, pp. 81–90. IEEE Computer Society Press (2006)
Ong, C.H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proceedings of POPL 2011, pp. 587–598. ACM (2011)
Ramsay, S.J., Neatherway, R.P., Ong, C.L.: A type-directed abstraction refinement approach to higher-order model checking. In: Proceedings of POPL 2014, pp. 61–72. ACM (2014)
Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Proceedings of PEPM 2013, pp. 53–62. ACM (2013)
Terao, T., Kobayashi, N.: A ZDD-based efficient higher-order model checking algorithm. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 354–371. Springer, Heidelberg (2014). doi:10.1007/978-3-319-12736-1_19
Terao, T., Tsukada, T., Kobayashi, N.: Higher-order model checking in direct style (2016). http://www-kb.is.s.u-tokyo.ac.jp/~terao/papers/aplas16.pdf
Tsukada, T., Kobayashi, N.: Complexity of model-checking call-by-value programs. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 180–194. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54830-7_12
Acknowledgment
This work was supported by JSPS KAKENHI Grant Numbers JP16J01038 and JP15H05706.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Terao, T., Tsukada, T., Kobayashi, N. (2016). Higher-Order Model Checking in Direct Style. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-47958-3_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47957-6
Online ISBN: 978-3-319-47958-3
eBook Packages: Computer ScienceComputer Science (R0)