Navegar

Colección

Datos Estadísticas

Artículo

Cuervo Parrino, B.; Galeotti, J.P.; Garbervetsky, D.; Frias, M.F. "A dataflow analysis to improve SAT-based bounded program verification" (2011) 9th International Conference on Software Engineering and Formal Methods, SEFM 2011. 7041 LNCS:138-154
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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. © 2011 Springer-Verlag.

Registro:

Documento: Artículo
Título:A dataflow analysis to improve SAT-based bounded program verification
Autor:Cuervo Parrino, B.; Galeotti, J.P.; Garbervetsky, D.; Frias, M.F.
Ciudad:Montevideo
Filiación:Departmento de Computación, FCEyN, UBA, Argentina
CONICET, Argentina
Department of Software Engineering, ITBA, Argentina
Palabras clave:Bounded program verifications; Empirical evaluations; Logical representations; NP complete problems; Propositional formulas; Propositional variables; SAT solvers; SAT-based bounded verification; Verification tools; Computational complexity; Data flow analysis; Formal logic; Program translators; Verification; Formal methods
Año:2011
Volumen:7041 LNCS
Página de inicio:138
Página de fin:154
DOI: http://dx.doi.org/10.1007/978-3-642-24690-6_11
Título revista:9th International Conference on Software Engineering and Formal Methods, SEFM 2011
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7041LNCS_n_p138_CuervoParrino

Referencias:

  • Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on Java predicates (2002) ISSTA 2002, pp. 123-133
  • Belt, J., Robby, Deng, X., Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analyses (2009) FSE 2009, pp. 355-364
  • Biere, A., Heule, M., Van Maaren, H., Handbook of Satisfiability (2009) Frontiers in Artificial Intelligence and Applications, 185
  • Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M., (2011) A Dataflow Analysis to Improve SAT-based Program Verification, , http://www.dc.uba.ar/tacoflow/techrep.pdf, Technical Report May
  • 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), pp. 451-490
  • Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E., Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4111 LNCS, pp. 342-363. , Formal Methods for Components and Objects - 4th International Symposium, FMCO 2005, Revised Lectures
  • Dennis, G., Yessenov, K., Jackson, D., Bounded Verification of Voting Software (2008) LNCS, 5295, pp. 130-145. , Shankar, N., Woodcock, J. (eds.) VSTTE 2008. Springer, Heidelberg
  • Frias, M.F., Galeotti, J.P., Lopez Pombo, C.G., Aguirre, N., DynAlloy: Upgrading Alloy with Actions (2005) ICSE 2005, pp. 442-450
  • Galeotti, J., (2011) Software Verification Using Alloy, , PhD. Thesis, UBA
  • Galeotti, J.P., Rosner, N., López Pombo, C.G., Frias, M.F., Analysis of invariants for efficient bounded verification (2010) Proceedings of ISSTA 2010, pp. 25-36
  • Harel, D., Kozen, D., Tiuryn, J., (2000) Dynamic Logic, , Foundations of Computing. MIT Press, Cambridge
  • Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P., F-Soft: Software Verification Platform (2005) LNCS, 3576, pp. 301-306. , Etessami, K., Rajamani, S.K. (eds.) CAV 2005. Springer, Heidelberg
  • Jackson, D., (2006) Software Abstractions, , MIT Press, Cambridge
  • Jackson, D., Vaziri, M., Finding bugs with a constraint solver (2000) ISSTA 2000, pp. 14-25
  • Kindall, G.A., A unified approach to global program optimization (1973) POPL 1973, pp. 194-206
  • De Moura, L., Bjørner, N.S., Z3: An Efficient SMT Solver (2008) LNCS, 4963, pp. 337-340. , Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. Springer, Heidelberg
  • Nielson, F., A denotational framework for data flow analysis (1982) Acta Inf., 18, pp. 265-287
  • Shao, D., Gopinath, D., Khurshid, S., Perry, D.E., Optimizing Incremental Scope-Bounded Checking with Data-Flow Analysis (2010) ISSRE 2010, pp. 408-417
  • Sharma, R., Gligoric, M., Arcuri, A., Fraser, G., Marinov, D., Testing Container Classes: Random or Systematic? (2011) LNCS, 6603, pp. 262-277. , Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. Springer, Heidelberg
  • Siddiqui, J.H., Khurshid, S., An Empirical Study of Structural Constraint Solving Techniques (2009) LNCS, 5885, pp. 88-106. , Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. Springer, Heidelberg
  • Torlak, E., Jackson, D., Kodkod: A Relational Model Finder (2007) LNCS, 4424, pp. 632-647. , Grumberg, O., Huth, M. (eds.) TACAS 2007. Springer, Heidelberg
  • Taghdiri, M., Seater, R., Jackson, D., Lightweight extraction of Syntactic Specifications (2006) FSE 2006, pp. 276-286
  • Visser, W., Pǎ;sǎ;reanu, C.S., Pelánek, R., Test Input Generation for Java Containers using State Matching (2006) ISSTA 2006, pp. 37-48
  • Xie, Y., Aiken, A., Saturn: A scalable framework for error detection using Boolean satisfiability (2007) ACM TOPLAS, 29 (3)A4 - Agencia Nacional de Investigacion e Innovacion (ANII); Univ. Repub., Com. Sect. Invest. Cient. (CSIC); Programa Desarro. Cienc. Basicas (PEDECIBA) Inform.

Citas:

---------- APA ----------
Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D. & Frias, M.F. (2011) . A dataflow analysis to improve SAT-based bounded program verification. 9th International Conference on Software Engineering and Formal Methods, SEFM 2011, 7041 LNCS, 138-154.
http://dx.doi.org/10.1007/978-3-642-24690-6_11
---------- CHICAGO ----------
Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.F. "A dataflow analysis to improve SAT-based bounded program verification" . 9th International Conference on Software Engineering and Formal Methods, SEFM 2011 7041 LNCS (2011) : 138-154.
http://dx.doi.org/10.1007/978-3-642-24690-6_11
---------- MLA ----------
Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.F. "A dataflow analysis to improve SAT-based bounded program verification" . 9th International Conference on Software Engineering and Formal Methods, SEFM 2011, vol. 7041 LNCS, 2011, pp. 138-154.
http://dx.doi.org/10.1007/978-3-642-24690-6_11
---------- VANCOUVER ----------
Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.F. A dataflow analysis to improve SAT-based bounded program verification. Lect. Notes Comput. Sci. 2011;7041 LNCS:138-154.
http://dx.doi.org/10.1007/978-3-642-24690-6_11