Abstract
SAT-based bounded verification of programs consists of the translation of the code and its annotations into a propositional formula. The formula is then analyzed for specification violations using a SAT-solver. This technique is capable of proving the absence of errors up to a given scope. SAT is a well-known NP-complete problem, whose complexity depends on the number of propositional variables occurring in the formula. Thus, reducing the number of variables in the logical representation may have a great impact on the overall analysis. We propose a dataflow analysis which infers the set of possible values that can be assigned to each local and instance variable. Unnecessary variables at the SAT level can then be safely removed by relying on the inferred values. We implemented this approach in TACO, a SAT-based verification tool. We present an extensive empirical evaluation and discuss the benefits of the proposed approach.
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
Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA 2002, pp. 123–133 (2002)
Belt J., Robby, Deng X.: Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analyses. In: FSE 2009, pp. 355–364 (2009)
Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185 (2009)
Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.: A dataflow analysis to improve SAT-based program verification, Technical Report (May 2011), http://www.dc.uba.ar/tacoflow/techrep.pdf
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM TOPLAS 13(4), 451–490
Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)
Dennis, G., Yessenov, K., Jackson, D.: Bounded Verification of Voting Software. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 130–145. Springer, Heidelberg (2008)
Frias, M.F., Galeotti, J.P., Lopez Pombo, C.G., Aguirre, N.: DynAlloy: Upgrading Alloy with Actions. In: ICSE 2005, pp. 442–450 (2005)
Galeotti, J.: Software Verification Using Alloy. PhD. Thesis, UBA (2011)
Galeotti, J.P., Rosner, N., López Pombo, C.G., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Proceedings of ISSTA 2010, pp. 25–36 (2010)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. Foundations of Computing. MIT Press, Cambridge (2000)
Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software Verification Platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301–306. Springer, Heidelberg (2005)
Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)
Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA 2000, pp. 14–25 (2000)
Kindall, G.A.: A unified approach to global program optimization. In: POPL 1973, pp. 194–206 (1973)
de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Nielson, F.: A denotational framework for data flow analysis. Acta Inf. 18, 265–287 (1982)
Shao, D., Gopinath, D., Khurshid, S., Perry, D.E.: Optimizing Incremental Scope-Bounded Checking with Data-Flow Analysis. In: ISSRE 2010, pp. 408–417 (2010)
Sharma, R., Gligoric, M., Arcuri, A., Fraser, G., Marinov, D.: Testing Container Classes: Random or Systematic? In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 262–277. Springer, Heidelberg (2011)
Siddiqui, J.H., Khurshid, S.: An Empirical Study of Structural Constraint Solving Techniques. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 88–106. Springer, Heidelberg (2009)
Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)
Taghdiri, M., Seater, R., Jackson, D.: Lightweight extraction of Syntactic Specifications. In: FSE 2006, pp. 276–286 (2006)
Visser, W., Păsăreanu, C.S., Pelánek, R.: Test Input Generation for Java Containers using State Matching. In: ISSTA 2006, pp. 37–48 (2006)
Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using Boolean satisfiability. ACM TOPLAS 29(3) (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.F. (2011). A Dataflow Analysis to Improve SAT-Based Bounded Program Verification. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-24690-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24689-0
Online ISBN: 978-3-642-24690-6
eBook Packages: Computer ScienceComputer Science (R0)