Abstract
Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. In this context Boolean programs are commonly employed as simple, yet useful abstractions from conventional programming languages. In this paper we propose Linear Programs as a finer grained abstraction for sequential programs and propose a model checking procedure for this family of programs. We also present the eureka toolkit, which consists of a prototype implementation of our model checking procedure for Linear Programs as well as of a library of Linear Programs to be used for benchmarking. Experimental results obtained by running our model checker against the library provide evidence of the effectiveness of the approach.
We are indebted to Pasquale De Lucia for his contribution to the development of a preliminary version of the model checker described in this paper.
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.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems 21, 747–789 (1999)
Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23, 279–295 (1997)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Z.H.: Bandera: extracting finite-state models from java source code. In: Proc. of the 22nd int. conf. on Software engineering, pp. 439–448. ACM Press, New York (2000)
Visser, W., Havelund, K., Brat, G., Park, S.: Java pathfinder - second generation of a java model checker (2000)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Proc. of the 25th int. conf. on Software engineering, pp. 385–395. IEEE Computer Society Press, Los Alamitos (2003)
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., Kröning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI–C programs using SAT. In: FMSD (to appear, 2004)
Flanagan, C.: Automatic software model checking using CLP. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 189–203. Springer, Heidelberg (2003)
Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Software Testing, Verification and Reliability 11, 65–79 (2001)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT POPL Symposium, pp. 84–97. ACM Press, New York (1978)
Cousot, P., Cousot, R.: Comparison of the Galois connection and widening/narrowing approaches to abstract interpretation. JTASPEFL 1991, Bordeaux. BIGRE 74, 107–110 (1991)
de Moura, L., Ruess, H., Shankar, N., Rushby, J.: The ICS decision procedure for embedded deduction. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol. 3097, pp. 218–222. Springer, Heidelberg (2004)
Chen, H., Wagner, D.: MOPS: an infrastructure for examining security properties of software. In: Proceedings of the 9th ACM Conference on Computer and Communications Security, Washington, DC, pp. 235–244 (2002)
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universität München (2002)
Weissenbacher, G.: An Abstraction/Refinement Scheme for Model Checking C Programs. PhD thesis, Technische Universität Graz (2003)
Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. In: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pp. 14–24. ACM Press, New York (2004)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58–70 (2002)
Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The omega library interface guide. Technical report, Univ. of Maryland at College Park (1995)
Armando, A., Castellini, C., Mantovani, J.: Introducing full linear arithmetic to symbolic software model checking. Technical report, University of Genova (2004), Available at : http://www.ai.dist.unige.it/eureka
Armando, A., de Lucia, P.: Symbolic model-checking of linear programs. Technical report, Datalogiske Skrifter, Technical Report No. 94, Roskilde University (2002)
Lassez, J.L., Maher, M.: On Fourier’s Algorithm’s for Linear Arithmetic Constraints. JAR 9, 373–379 (1992)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. POPL 95, 49–61 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armando, A., Castellini, C., Mantovani, J. (2004). Software Model Checking Using Linear Constraints. In: Davies, J., Schulte, W., Barnett, M. (eds) Formal Methods and Software Engineering. ICFEM 2004. Lecture Notes in Computer Science, vol 3308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30482-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-30482-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23841-6
Online ISBN: 978-3-540-30482-1
eBook Packages: Springer Book Archive