Abstract
This paper presents a new compositional approach for safety verification of C programs. A program is represented by a sequence of assignments and a sequence of guarded blocks. Abstraction consists to abstract the program in a set of blocks relevant to the erroneous location (EL). As in the CEGAR paradigm, the abstracted model is used to prove or disprove the property. This checking is performed for each block backwardly, using Weakest Preconditions to generate a formula which Satisfiability is checked. If the abstraction is too coarse to allow deciding on the Satisfiability of the formula, then a path-guided refinement is performed. Our technique allows handling programs containing function calls and pointers. All aspects described in this paper are illustrated by clarifying examples.
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
Preview
Unable to display preview. Download preview PDF.
References
Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL, pp. 1–3. ACT, New York (2002)
Ball, T., Bounimova, E., Kumar, R., Levin,V.: Slam2: Static Driver Verification with Under 4% False Alarms. In: FMCAD (2010)
Ball, T., Majumdar, R., Rajamani, S.: Automatic predicate abstraction of C programs. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 203–213 (2001)
Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The Blast Query Language for Software Verification. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 2–18. Springer, Heidelberg (2004)
Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software Model Checking via Large-Block Encoding
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)
Dijkstra, E.: A discipline of programming. Prentice-Hall (1976)
Gulavani, B., Henzinger, T.A., Kannan, Y., Nori, A., Rajamani, S.K.: Synergy: a new algorithm for property checking. In: Proc. FSE. ACT, New York (2006)
Nori, A.V., Rajamani, S.K.: An Empirical Study of Optimizations in Yogi. In: ICSE 2010: International Conference on Software Engineering (May 2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Aleb, N., Kechid, S. (2013). Path Guided Abstraction Refinement for Safety Program Verification. In: Nagamalai, D., Kumar, A., Annamalai, A. (eds) Advances in Computational Science, Engineering and Information Technology. Advances in Intelligent Systems and Computing, vol 225. Springer, Heidelberg. https://doi.org/10.1007/978-3-319-00951-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-00951-3_12
Publisher Name: Springer, Heidelberg
Print ISBN: 978-3-319-00950-6
Online ISBN: 978-3-319-00951-3
eBook Packages: EngineeringEngineering (R0)