Slicing Abstractions

• Autorzy: Brückner I. , Dräger K. , Finkbeiner B. , Wehrheim H.
• Języki publikacji: EN

Abstrakty

EN

Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for infinite-state concurrent systems that interleaves automatic abstraction refinement, which splits states according to new predicates obtained by Craig interpolation, with slicing, which removes irrelevant states and transitions from the abstraction. The effects of abstraction and slicing complement each other. As the refinement progresses, the increasing accuracy of the abstract model allows for a more precise slice; the resulting smaller representation gives room for additional predicates in the abstraction. The procedure terminates when an error path in the abstraction can be concretized, which proves that the system is erroneous, or when the slice becomes empty, which proves that the system is correct.

Słowa kluczowe

EN

verification; slicing; Craig interpolation; abstraction

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 89, nr 4
• Strony: 369--392
• Opis fizyczny: bibliogr. 36 poz., tab., wykr.

Twórcy

autor

Brückner I.

autor

Dräger K.

autor

Finkbeiner B.

autor

Wehrheim H.

• Fachrichtung Informatik Universität des Saarlandes 66123 Saarbrücken, Germany,

Bibliografia

• [1] de Alfaro, L., Henzinger, T. A., Mang, F. Y. C.: Detecting Errors Before Reaching Them, Proc. CAV '00 (E. A. Emerson, A. P. Sistla, Eds.), 1855, Springer, 2000, ISBN 3-540-67770-4.
• [2] Ball, T., Cook, B., Das, S., Rajamani, S. K.: Refining Approximations in Software Predicate Abstraction, Proc. TACAS '04 (K. Jensen, A. Podelski, Eds.), 2988, Springer-Verlag, 2004, ISBN 3-540-21299-X.
• [3] Ball, T., Podelski, A., Rajamani, S. K.: Boolean and Cartesian Abstraction for Model Checking C Programs, Proc. TACAS '01 (T. Margaria,W. Yi, Eds.), Springer-Verlag, 2001, ISBN 3-540-41865-2.
• [4] Ball, T., Rajamani, S. K.: Automatically validating temporal safety properties of interfaces, Proc. SPIN '01 (M. B. Dwyer, Ed.), Springer-Verlag New York, Inc., New York, NY, USA, 2001, ISBN 3-540-42124-6.
• [5] Baumgartner, J., Kuehlmann, A., Abraham, J. A.: Property Checking via Structural Analysis, Proc. CAV '00 (E. Brinksma, K. G. Larsen, Eds.), 2404, Springer, 2002, ISBN 3-540-43997-8.
• [6] Bozga, M., Fernandez, J.-C., Ghirvu, L., Graf, S., Krimm, J.-P., Mounier, L.: IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems, World Congress on Formal Methods (J. M. Wing, J. Woodcock, J. Davies, Eds.), 1708, Springer, 1999, ISBN 3-540-66587-0.
• [7] Brückner, I., Dräger, K., Finkbeiner, B.,Wehrheim, H.: Slicing Abstractions, Proc. FSEN'07, 4767, Springer- Verlag, 2007, ISBN 978-3-540-75697-2.
• [8] Canfora, G., Cimitile, A., Lucia, A. D.: Conditioned program slicing, Information and Software Technology, Special Issue on Program Slicing, 40, 1998, 595-607.
• [9] Chaki, S., Clarke, E. M., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C, IEEE Trans. Software Eng., 30(6), 2004, 388-402.
• [10] Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement, Proc. CAV '00 (E. A. Emerson, A. P. Sistla, Eds.), Springer-Verlag, London,UK, 2000, ISBN 3-540-67770-4.
• [11] Clarke, E. M., Grumberg, O., Talupur, M., Wang, D.: Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates, Proc. CAV '03 (W. A. H. Jr., F. Somenzi, Eds.), 2725, Springer, 2003, ISBN 3-540-40524-0.
• [12] Colón, M. A., Uribe, T. E.: Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures, Proc. CAV '98 (A. J. Hu, M. Y. Vardi, Eds.), 1427, Springer-Verlag, July 1998.
• [13] Das, S., Dill, D. L.: Counter-Example Based Predicate Discovery in Predicate Abstraction, Proc. FMCAD '02 (M. Aagaard, J. W. O'Leary, Eds.), Springer-Verlag, November 2002.
• [14] Dwyer, M. B., Hatcliff, J., Hoosier, M., Ranganath, V., Robby, Wallentine, T.: Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs, Proc. TACAS'06 (H. Hermanns, J. Palsberg, Eds.), 3920, Springer, 2006, ISBN 3-540-33056-9.
• [15] Fox, C., Danicic, S., Harman, M., Hierons, R. M.: Backward Conditioning: A New Program Specialisation Technique and Its Application to Program Comprehension, Proc. IWPC' 01, IEEE Computer Society, 2001, ISBN 0-7695-1131-7.
• [16] Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems, Ph.D. Thesis, Université de Liege, 1994.
• [17] Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS, Proc. CAV '97 (O. Grumberg, Ed.), 1254, Springer-Verlag, June 1997.
• [18] Henzinger, T., Jhala, R., Majumdar, R., SUTRE, G.: Lazy Abstraction, Proc. POPL '02, ACM Press, 2002.
• [19] Henzinger, T. A., Jhala, R., Majumdar, R., McMillan, K. L.: Abstractions from proofs, Proc. POPL '04 (N. D. Jones, X. Leroy, Eds.), ACM Press, New York, NY, USA, 2004, ISBN 1-58113-729-X.
• [20] Henzinger, T. A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST, Proc. SPIN '03 (T. Ball, S. K. Rajamani, Eds.), 1427, Springer-Verlag, 2003.
• [21] Holzmann, G. J., Peled, D.: An improvement in formal verification, Proc. FORTE '94 (D. Hogrefe, S. Leue, Eds.), 6, Chapman & Hall, 1994, ISBN 0-412-64450-9.
• [22] Hong, H., Lee, I., Sokolsky, O.: Abstract Slicing: A New Approach to Program Slicing Based on Abstract Interpretation and Model Checking., Proc. SCAM '05, IEEE Computer Society, 2005, ISBN 0-7695-2292-0.
• [23] Jhala, R., Majumdar, R.: Path slicing, Proc. PLDI '05 (V. Sarkar, M. W. Hall, Eds.), ACM Press, New York, NY, USA, 2005, ISBN 1-59593-056-6.
• [24] Lamport, L.: A New Solution of Dijkstra's concurrent programming problem, Communications of the ACM, 17(8), 1974, 435-455.
• [25] Manna, Z., Pnueli, A.: Clocked Transition Systems, Technical Report STAN-CS-TR-96-1566, Computer Science Department, Stanford University, April 1996.
• [26] McMillan, K. L.: Applications of Craig Interpolants in Model Checking., Proc. TACAS '05 (N. Halbwachs, L. D. Zuck, Eds.), 3440, Springer-Verlag, 2005, ISBN 3-540-25333-5.
• [27] McMillan, K. L.: Lazy Abstraction with Interpolants., Proc. CAV '06 (T. Ball, R. B. Jones, Eds.), 4144, Springer, 2006, ISBN 3-540-37406-X.
• [28] Millett, L., Teitelbaum, T.: Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation, Software Tools for Technology Transfer, 2(4), 2000, 343-349.
• [29] Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement, Proc. PADL '07 (M. Hanus, Ed.), 4354, Springer-Verlag, 2007.
• [30] Rybalchenko, A.: CLP-Prover, http://www.mpi-sws.mpg.de/_rybal/clp-prover/, 2006.
• [31] Sipma, H. B., Uribe, T. E., Manna, Z.: Deductive Model Checking, Formal Methods in System Design, 15(1), July 1999, 49-74, Preliminary version appeared in Proc. 8th Intl. Conference on Computer Aided Verification, vol. 1102 of LNCS, Springer-Verlag, pp. 208-219, 1996.
• [32] V. Ganesh, H. Saidi, N. S.: Slicing SAL, Technical report, SRI International, http://theory.stanford.edu/, 1999.
• [33] Vasudevan, S., Emerson, E. A., Abraham, J. A.: Efficient Model Checking of Hardware Using Conditioned Slicing, ENTCS, 128(6), 2005, 279-294.
• [34] Visser, W., Havelund, K., Brat, G. P., Park, S., Lerda, F.: Model Checking Programs, Autom. Softw. Eng., 10(2), 2003, 203-232.
• [35] Weiser, M.: Program slicing, Proc. ICSE '81, IEEE Press, 1981, ISBN 0-89791-146-6.
• [36] Yang, C. H., Dill, D. L.: Validation with Guided Search of the State Space, Proc. DAC '98, 1998.