Abstract
Automatically generating assertions through static or runtime analysis is becoming an increasingly important initial phase in many software testing and verification tool chains. The analyses may generate thousands of redundant assertions often causing problems later in the chain, including scalability issues for automatic tools or a prohibitively large amount of information for final processing. We present an algorithm which uses a SAT solver on a bounded symbolic encoding of the program to reveal the implication relationships among spatially close assertions for use in a variety of bounded model checking applications. Our experimentation with different applications demonstrates that this technique can be used to reduce the number of assertions that need to be checked thus improving overall performance.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The openSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010)
Cabodi, G., Lolacono, C., Vendraminetto, D.: Optimization techniques for Craig interpolant compaction in unbounded model checking. In: DATE 2013, pp. 1417–1422. ACM DL, EDA Consortium San Jose (2013)
Clarke, E., Kroning, 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.M., Emerson, A.: Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, Springer, Heidelberg (1982)
Cobb, J., Jones, J.A., Kapfhammer, G.M., Harrold, M.J.: Dynamic invariant detection for relational databases. In: Proc. International Workshop on Dynamic Analysis 2011, pp. 12–17. ACM (2011)
Craig, W.: Three uses of the Herbrand-Genzen theorem in relating model theory and proof theory. JSL 22(3), 269–285 (1957)
Dodoo, N., Donovan, A., Lin, L., Ernst, M.D.: Selecting predicates for implications in program analysis (2002), http://homes.cs.washington.edu/~mernst/pubs/invariants-implications.ps
Donaldson, A.F., Kroening, D., Rümmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 280–295. Springer, Heidelberg (2010)
Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering 27(2), 99–123 (2001)
Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: Incremental Upgrade Checker for C. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 292–307. Springer, Heidelberg (2013)
Fedyukovich, G., Sharygina, N.: Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection. In: Braga, C., Martí-Oliet, N. (eds.) SBMF 2014. LNCS, vol. 8941, pp. 96–112. Springer, Heidelberg (2015)
Flanagan, C., Rustan, K., Leino, M.: Houdini, an annotation assistant for eSC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)
Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. TCS 404(3), 256–274 (2008)
Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using state and transition invariants. Formal Methods in System Design 42(3), 221–261 (2013)
Lal, A., Qadeer, S.: A program transformation for faster goal-directed search. In: Proc. FMCAD 2014, pp. 147–154. IEEE (2014)
Mariani, L., Pastore, F., Pezzè, M.: Dynamic analysis for diagnosing integration faults. IEEE Transactions on Software Engineering 37(4), 486–508 (2011)
Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146–161. Springer, Heidelberg (2012)
Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: Proc. ICSE 2012, pp. 683–693. IEEE (2012)
Pastore, F., Mariani, L., Hyvärinen, A.E.J., Fedyukovich, G., Sharygina, N., Sehestedt, S., Muhammad, A.: Verification-aided regression testing. In: Proc. ISSTA 2014, pp. 37–48. ACM (2014)
Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic 62(3), 981–998 (1997)
Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)
Rollini, S.F., Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: PeRIPLO: A framework for producing effective interpolants in SAT-based software verification. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 683–693. Springer, Heidelberg (2013)
Sery, O., Fedyukovich, G., Sharygina, N.: FunFrog: Bounded model checking with interpolation-based function summarization. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 203–207. Springer, Heidelberg (2012)
Weiser, M.: Program slicing. In: Proc. ICSE 1981, pp. 439–449. IEEE (1981)
Yang, G., Khurshid, S., Person, S., Rungta, N.: Property differencing for incremental checking. In: Proc. ICSE 2014, pp. 1059–1070. ACM (2014)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fedyukovich, G., D’Iddio, A.C., Hyvärinen, A.E.J., Sharygina, N. (2015). Symbolic Detection of Assertion Dependencies for Bounded Model Checking. In: Egyed, A., Schaefer, I. (eds) Fundamental Approaches to Software Engineering. FASE 2015. Lecture Notes in Computer Science(), vol 9033. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46675-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-662-46675-9_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46674-2
Online ISBN: 978-3-662-46675-9
eBook Packages: Computer ScienceComputer Science (R0)