Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
Tóm tắt
In this article, we investigate the automated verification of temporal properties of heap-aware programs. We propose a deductive reasoning approach based on cyclic proof. Judgements in our proof system assert that a program has a certain temporal property over memory state assertions, written in separation logic with user-defined inductive predicates, while the proof rules of the system unfold temporal modalities and predicate definitions as well as symbolically executing programs. Cyclic proofs in our system are, as usual, finite proof graphs subject to a natural, decidable soundness condition, encoding a form of proof by infinite descent. We present a proof system tailored to proving CTL properties of nondeterministic pointer programs, and then adapt this system to handle fair execution conditions. We show both versions of the system to be sound, and provide an implementation of each in the Cyclist theorem prover, yielding an automated tool that is capable of automatically discovering proofs of (fair) temporal properties of pointer programs. Experimental evaluation of our tool indicates that our approach is viable, and offers an interesting alternative to traditional model checking techniques.
Tài liệu tham khảo
https://github.com/ngorogiannis/cyclist/releases/tag/JAR
Berdine, J., Calcagno, C., O’Hearn, P.W.: A decidable fragment of separation logic. In: Proceedings of FSTTCS-24, pp. 97–109. Springer, Berlin (2004)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast: applications to software engineering. Int. J. Softw. Tools Technol. Transfer 9, 505–525 (2007)
Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for CTL*. In: Proceedings of LICS-10, pp. 388–397. IEEE (1995)
Brotherston, J.: Sequent calculus proof systems for inductive definitions. Ph.D. thesis, University of Edinburgh (2006)
Brotherston, J.: Formalised inductive reasoning in the logic of bunched implications. In: Proceedings of SAS-14, LNCS, vol. 4634, pp. 87–103. Springer, Berlin (2007)
Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: Proceedings of POPL-35, pp. 101–112. ACM (2008)
Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: Proceedings of SAS-21, LNCS, vol. 8723, pp. 68–84. Springer, Berlin (2014)
Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Proceedings of APLAS-10, LNCS, pp. 350–367. Springer, Berlin (2012)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proceedings of TACAS, LNCS, vol. 2988, pp. 168–176. Springer, Berlin (2004)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. Logic of Programs. Workshop, pp. 52–71. Springer, Berlin (1981)
Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: Proceedings of POPL-34, POPL ’07, pp. 265–276. ACM (2007)
Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* verification for infinite-state systems. In: Proceedings of CAV-27, LNCS, vol. 9206. Springer, Berlin (2015)
Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: Proceedings of POPL-38, vol. 46, pp. 399–410. ACM (2011)
Cook, B., Koskinen, E.: Reasoning about nondeterminism in programs. In: Proceedings of PLDI-34, pp. 219–230. ACM (2013)
Dam, M.: Translating CTL* Into the Modal Mu-calculus. ECS-LFCS-.University of Edinburgh, Department of Computer Science, Laboratoryfor Foundations of Computer Science (1990)
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not never” revisited: on branching versus linear time temporal logic. J. ACM 33, 151–178 (1986)
Fix, L., Grumberg, O.: Verification of temporal properties. J. Log. Comput. 6, 343–361 (1996)
Hungar, H., Grumberg, O., Damm, W.: What if model checking must be truly symbolic. In: Proceedings of CHARME, pp. 1–20. Springer, Berlin (1995)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 125–143 (1977)
Löding, C., Thomas, W.: Methods for the transformation of \(\omega \)-automata: complexity and connection to second order logic (2007)
Magill, S., Tsai, M.H., Lee, P., Tsay, Y.K.: Automatic numeric abstractions for heap-manipulating programs. In: Proceedings of the 37th Annual Symposium on Principles of Programming Languages, POPL ’10, pp. 211–222. ACM (2010)
Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 97–130 (1991)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Proceedings of the 5th CISP, pp. 337–351. Springer, Berlin (1982)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings LICS-17, pp. 55–74. IEEE (2002)
Rowe, R.N.S., Brotherston, J.: Automatic cyclic termination proofs for recursive procedures in separation logic. In: Proceedings of CPP-6. ACM (2016)
Schopp, U., Simpson, A.: Verifying temporal properties using explicit approximants: completeness for context-free processes. In: Proceedings of FoSSaCS, pp. 372–386. Springer, Berlin (2002)
Sprenger, C.: Deductive local model checking—on the verification of ctl* properties of infinite-state reactive systems. Ph.D. thesis, Swiss Federal Institute of Technology (2000)
Sprenger, C., Dam, M.: On the structure of inductive reasoning: circular and tree-shaped proofs in the \(\mu \)-calculus. In: Proceedings of FOSSACS 2003, LNCS, vol. 2620, pp. 425–440. Springer, Berlin (2003)
Tellez, G., Brotherston, J.: Automatically verifying temporal properties of pointer programs with cyclic proof. In: Automated Deduction—CADE 26, pp. 491–508. Springer, Berlin (2017)
Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Proceedings of CONCUR-18, pp. 256–271. Springer, Berlin (2007)
Vardi, M.Y.: Verification of concurrent programs: the automata-theoretic framework*. Ann. Pure Appl. Logic 51(1), 79–98 (1991)
Visser, W., Barringer, H.: Practical CTL* model checking: should spin be extended? Int. J. Softw. Tools Technol. Transfer 2(4), 350–365 (2000)