Abstract
Software verification is a hard yet important challenge. In general, the problem is undecidable. Nevertheless, it is still beneficial to look at solutions that either restrict the generality or are heuristic in nature (and do not guarantee to terminate). In this paper, we concentrate on a related problem, that of verifying that a cycle in the flow chart of a program does not terminate. We show some exact and sufficient conditions for cycle nontermination, and provide application for program verification. This allows us to check sequential and concurrent programs against temporal properties, using a truly symbolic approach, and to use temporal logic to guide the selection of test cases in such programs.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. FMICS 2002, Malaga, Spain, ENTCS 66(2) (2002)
Bosnacki, D., et al.: On Commutativity Based Edge Lean Search. In: Arge, L., et al. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 158–170. Springer, Heidelberg (2007)
Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006, Ottawa, Ontario, Canada, pp. 415–426 (2006)
Floyd, R.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19–32 (1967)
Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simpler on-the-fly automatic Cverification of linear temporal logic. In: PSTV 1995, Warsaw, Poland, pp. 3–18 (1995)
Godefroid, P., Wolper, P.: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 176–185. Springer, Heidelberg (1992)
Gunter, E.L., Peled, D.: Unit Checking: Symbolic Model Checking for a Unit of Code. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 548–567. Springer, Heidelberg (2004)
Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communication ACM 12(10), 576–580 (1969)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1990)
Matiyasevich, Y.V.: Hilbert’s 10th Problem. MIT Press, Cambridge (1993)
Mazurkiewicz, A.W.: Basic Notions of Trace Theory. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 285–363. Springer, Heidelberg (1989)
Pnueli, A.: The Temporal Logic of Programs. In: FOCS 1977, Rhode Island, pp. 46–57 (1977)
Podelski, A., Rybalchenko, A.: A Complete Method for the Synthesis of Linear Ranking Functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, Springer, Heidelberg (2004)
Podelski, A., Rybalchenko, A.: Transition Invariants. LICS 2004, 32–41, Turku, Finland (2004)
Queille, J.-P., Sifakis, J.: Iterative Methods for the Analysis of Petri Nets. In: Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets Bad Honnef, Informatik-Fachberichte 52, pp. 161–167 (1981)
Wolfram, S.: The Mathematica Book, 5th edn, Wolfram Media (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bensalem, S., Peled, D., Qu, H., Tripakis, S., Zuck, L. (2008). Test Case Generation for Ultimately Periodic Paths. In: Yorav, K. (eds) Hardware and Software: Verification and Testing. HVC 2007. Lecture Notes in Computer Science, vol 4899. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77966-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-77966-7_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77964-3
Online ISBN: 978-3-540-77966-7
eBook Packages: Computer ScienceComputer Science (R0)