Abstract
Temporal logic is a formal system for specifying and reasoning about propositions qualified in terms of time. It offers a unified approach to program verification as it applies to both sequential and parallel programs and provides a uniform framework for describing a system at any level of abstraction. Thus, a number of automated systems have been proposed to exclusively reason about either Computation-Tree Logic (CTL) or Linear Temporal Logic (LTL) in the infinite-state setting. Unfortunately, these logics have significantly reduced expressiveness as they restrict the interplay between temporal operators and path quantifiers, thus disallowing the expression of many practical properties, for example, “along some future an event occurs infinitely often.” Contrarily, CTL*, a superset of both CTL and LTL, can facilitate the interplay between path-based and state-based reasoning. CTL* thus exclusively allows for the expressiveness of properties involving existential system stabilization and “possibility” properties. Until now, there have not existed automated systems that allow for the verification of such expressive CTL* properties over infinite-state systems. This article proposes a method capable of such a task, thus introducing the first known fully automated tool for symbolically proving CTL* properties of (infinite-state) integer programs. The method uses an internal encoding that admits reasoning about the subtle interplay between the nesting of temporal operators and path quantifiers that occurs within CTL* proofs. A program transformation is first employed that trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. We then synthesize and quantify preconditions over the transformed program that represent program states that satisfy a CTL* formula.
This article demonstrates the viability of our approach in practice, thus leading to a new class of fully-automated tools capable of proving crucial properties that no tool could previously prove. Additionally, we consider the linear-past extension to CTL* for infinite-state systems in which the past is linear and each moment in time has a unique past. We discuss the practice of this extension and how it is further supported through the use of history variables. We have implemented our approach and report our benchmarks carried out on case studies ranging from smaller programs to demonstrate the expressiveness of CTL* specifications, to larger code bases drawn from device drivers and various industrial examples.
- Martín Abadi and Leslie Lamport. 1991. The existence of refinement mappings. Theoretical Computer Science 82 (1991), 253--284. Google ScholarDigital Library
- Bowen Alpern and Fred B. Schneider. 1986. Recognizing Safety and Liveness. Technical Report. Ithaca, NY.Google Scholar
- Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, and Abdullah Ustuner. 2006. Thorough static analysis of device drivers. SIGOPS Operating Systems Review 40 (April 2006), 73--85. Issue 4. DOI:http://dx.doi.org/10.1145/1218063.1217943 Google ScholarDigital Library
- Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko. 2014a. CTL+FO verification as constraint solving. In Proceedings of the 2014 International SPIN Symposium on Model Checking of Software (SPIN’14). ACM, New York, NY, 101--104. Google ScholarDigital Library
- Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. 2014b. A constraint-based approach to solving games on infinite graphs. In POPL’14. ACM, 221--233. Google ScholarDigital Library
- Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving existentially quantified horn clauses. In CAV’13. Springer, 869--882. Google ScholarDigital Library
- Nikolaj S. Bjørner, Anca Browne, Michael A. Colón, Bernd Finkbeiner, Zohar Manna, Henny B. Sipma, and Tomás E. Uribe. 2000. Verifying temporal properties of reactive systems: A STeP tutorial. Form. Methods Syst. Des. 16, 3 (2000), 227--270. Google ScholarDigital Library
- Eric Bodden. 2004. A lightweight LTL runtime verification tool for Java. In OOPSLA’04. ACM, 306--307. Google ScholarDigital Library
- Laura Bozzelli. 2008. The complexity of CTL* + linear past. In Proceedings of the Theory and Practice of Software, 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg.Google ScholarDigital Library
- Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman. 2016. T2: Temporal property verification. In TACAS’16 (To Appear).Google Scholar
- E. M. Clarke, O. Grumberg, and D. A. Peled. 1999. Model Checking.Google Scholar
- Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Y. Vardi. 2007. Proving that programs eventually do something good. In POPL’07. ACM, 265--276. Google ScholarDigital Library
- Byron Cook, Heidy Khlaaf, and Nir Piterman. 2014. Faster temporal reasoning for infinite-state programs. In FMCAD’14. FMCAD Inc, 16:75--16:82. Google ScholarCross Ref
- Byron Cook, Heidy Khlaaf, and Nir Piterman. 2015. Fairness for Infinite-State Systems. In TACAS’15. Springer Berlin Heidelberg, 384--398. Google ScholarDigital Library
- Byron Cook and Eric Koskinen. 2011. Making prophecies with decision predicates. In POPL’11. ACM, 399--410. Google ScholarDigital Library
- Byron Cook and Eric Koskinen. 2013. Reasoning about nondeterminism in programs. In PLDI’13. ACM, 219--230. Google ScholarDigital Library
- Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. lexicographic termination proving. In TACAS’13 (LNCS). Springer, 47--61. Google ScholarDigital Library
- Thomas H. Cormen, Clifford Stein, Ronald L. Rivest, and Charles E. Leiserson. 2001. Introduction to Algorithms (2nd ed.). McGraw-Hill Higher Education.Google ScholarDigital Library
- E. Allen Emerson and Joseph Y. Halpern. 1986. “Sometimes” and “not never”; revisited: On branching versus linear time temporal logic. J. ACM 33, 1 (1986), 151--178. Google ScholarDigital Library
- E. Allen Emerson and Charanjit S. Jutla. 1999. The complexity of tree automata and logics of programs. SIAM J. Comput. 29, 1 (1999), 132--158. Google ScholarDigital Library
- E. Allen Emerson and Chin-Laung Lei. 1987. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program. 8, 3 (1987), 275--306. Google ScholarDigital Library
- E. Allen Emerson and A. Prasad Sistla. 1984. Deciding branching time logic. In STOC’84. ACM, 14--24. Google ScholarDigital Library
- Dov Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. 1980. On the temporal analysis of fairness. In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’80). ACM, New York, NY, 163--173. Google ScholarDigital Library
- Alain Griffault and Aymeric Vincent. 2004. The mec 5 model-checker. In CAV’04 (LNCS). Springer, 488--491. Google ScholarCross Ref
- Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, and Ru-Gang Xu. 2008. Proving non-termination. SIGPLAN Not. 43, 1 (January 2008), 147--158. Google ScholarDigital Library
- Hans Kamp. 1968. Tense Logic and the Theory of Linear Order. PhD Thesis, UCLA.Google Scholar
- Yonit Kesten and Amir Pnueli. 2005. A compositional approach to CTL* verification. Theor. Comput. Sci. 331, 2--3 (2005), 397--428.Google ScholarDigital Library
- Orna Kupferman, Amir Pnueli, and Moshe Y. Vardi. 2012. Once and for All. J. Comput. Syst. Sci. 78 (2012), 981--996. Google ScholarDigital Library
- Leslie Lamport. 1980. “Sometime” is sometimes “not never”: On the temporal logic of programs. In POPL’80. ACM, 174--185. Google ScholarDigital Library
- F. Laroussinie and Ph. Schnoebelen. 1995. A hierarchy of temporal logics with past. In Selected Papers of the Eleventh Symposium on Theoretical Aspects of Computer Science (STACS’94). Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 303--324. Google ScholarDigital Library
- Orna Lichtenstein, Amir Pnueli, and Lenore D. Zuck. 1985. The glory of the past. In Proceedings of the Conference on Logic of Programs. Springer-Verlag, London, UK, 196--218. Google ScholarCross Ref
- Stephen Magill, Josh Berdine, Edmund M. Clarke, and Byron Cook. 2007. Arithmetic strengthening for shape analysis. In SAS’07. Springer, 419--436. Google ScholarCross Ref
- Zohar Manna and Amir Pnueli. 1995. Temporal Verification of Reactive Systems: Safety. Vol. 2. Springer. Google ScholarCross Ref
- Kenneth Lauchlin McMillan. 2006. Lazy abstraction with interpolants. In CAV’06 (LNCS), Vol. 4144. Springer, 123--136. Google ScholarDigital Library
- Amir Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (SFCS’77). IEEE Computer Society, Washington, D.C., 46--57. Google ScholarDigital Library
- Andreas Podelski and Andrey Rybalchenko. 2004. Transition invariants. In LICS. IEEE, 32--41. Google ScholarCross Ref
- Arthur Prior. 1957. Time and modality. (1957).Google Scholar
- Mark Reynolds. 2001. An axiomatization of full computation tree logic. J. Symbolic Logic 66, 3 (2001), pp. 1011--1057. Google ScholarCross Ref
- Fu Song and Tayssir Touili. 2012. Pushdown model checking for malware detection. In TACAS’12. ACM, 607--610. Google ScholarDigital Library
- Moshe Y. Vardi and Pierre Wolper. 1986. An automata-theoretic approach to automatic program verification (preliminary report). In LICS. 332--344.Google Scholar
Index Terms
- Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
Recommendations
Branching-time logics with path relativisation
We define extensions of the full branching-time temporal logic CTL^@? in which the path quantifiers are relativised by formal languages of infinite words, and consider its natural fragments obtained by extending the logics CTL and CTL^+ in the same way. ...
Efficient model checking via the equational /spl mu/-calculus
LICS '96: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer ScienceThis paper studies the use of an equational variant of the modal /spl mu/-calculus as a unified framework for efficient temporal logic model checking. In particular we show how an expressive temporal logic, CTL*, may be efficiently translated into the /...
Verifying Temporal Properties of Reactive Systems: A STeP Tutorial
We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verify ...
Comments