Navegar

Colección

Datos Estadísticas

Conferencia

Galeotti, J.P.; Rosner, N.; Pombo, C.G.L.; Frias, M.F. "Analysis of invariants for efficient bounded verification" (2010) 19th International Symposium on Software Testing and Analysis, ISSTA 2010:25-35
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor

Abstract:

SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this article we present TACO, a prototype tool which implements a novel, general and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate that allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading in the experiments we have carried out to an improvement on the efficiency of the analysis of orders of magnitude, compared to the non-instrumented SAT-based analysis. We show that, in some cases, our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking or SMT-solving. © 2010 ACM.

Registro:

Documento: Conferencia
Título:Analysis of invariants for efficient bounded verification
Autor:Galeotti, J.P.; Rosner, N.; Pombo, C.G.L.; Frias, M.F.
Ciudad:Trento
Filiación:Department of Computer Science, FCEyN Universidad de Buenos Aires, Argentina
Department of Software Engineering, Buenos Aires Institute of Technology (ITBA), Argentina
Palabras clave:Alloy; DynAlloy; KodKod; SAT-based code analysis; Static analysis; Automated techniques; Code analysis; DynAlloy; Execution trace; KodKod; Linked data structures; Orders of magnitude; Propositional formulas; Propositional variables; Prototype tools; SAT solvers; SAT-based bounded verification; SAT-solving; Sequential programs; Symmetry-breaking; Tight bound; Computer software selection and evaluation; Data structures; Java programming language; Software testing; Static analysis; Model checking
Año:2010
Página de inicio:25
Página de fin:35
DOI: http://dx.doi.org/10.1145/1831708.1831712
Título revista:19th International Symposium on Software Testing and Analysis, ISSTA 2010
Título revista abreviado:ISSTA - Proc. Int. Symp. Softw. Test. Anal.
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97816055_v_n_p25_Galeotti

Referencias:

  • Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D., Evaluating the "Small Scope Hypothesis", , http://sdg.csail.mit.edu/publications.html, downloadable from
  • Belt, J., Robby, Deng, X., Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-Based Analyses, FSE 2009, pp. 355-364
  • Bouillaguet, Ch., Kuncak, V., Wies, T., Zee, K., Rinard, M.C., Using first-order theorem provers in the jahob data structure verification system (2007) VMCAI, pp. 74-88
  • Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on java predicates (2002) ISSTA, pp. 123-133
  • Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E., Beyond assertions: Advanced specification and verification with JML and ESC/java2 FMCO 2005, pp. 342-363
  • Clarke, E., Kroening, D., Lerda, F., A tool for checking ANSI-C programs TACAS 2004, LNCS 2988, pp. 168-176
  • DeMillo, R.A., Lipton, R.J., Sayward, F.G., Hints on test data selection: Help for the practicing programmer (1978) IEEE Computer, pp. 34-41. , April
  • Deng, X., Robby, Hatcliff, J., Towards A case-optimal symbolic execution algorithm for analyzing strong properties of object-oriented programs (2007) SEFM, pp. 273-282
  • Dennis, G., Chang, F., Jackson, D., Modular verification of code with SAT (2006) ISSTA'06, pp. 109-120
  • Dennis, G., Yessenov, K., Jackson, D., Bounded verification of voting software (2008) VSTTE 2008, , Toronto, Canada, October
  • Dolby, J., Vaziri, M., Tip, F., Finding bugs efficiently with a SAT solver (2007) ESEC/FSE'07, pp. 195-204. , ACM Press
  • Flanagan, C., Leino, R., Lillibridge, M., Nelson, G., Saxe, J., Stata, R., Extended static checking for java (2002) PLDI, pp. 234-245
  • Frias, M.F., Galeotti, J.P., Lopez Pombo, C.G., Aguirre, N., DynAlloy: Upgrading alloy with actions (2005) ICSE'05, pp. 442-450
  • Frias, M.F., Lopez Pombo, C.G., Galeotti, J.P., Aguirre, N., Efficient analysis of DynAlloy specifications (2007) ACM-TOSEM, 17 (1)
  • Galeotti, J.P., Frias, M.F., DynAlloy as a formal method for the analysis of java programs (2006) Proceedings of IFIP Working Conference on Software Engineering Techniques, , Warsaw Springer
  • Iosif, R., Symmetry reduction criteria for software model checking SPIN 2002, pp. 22-41
  • Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P., F-soft: Software verification platform (2005) CAV'05, pp. 301-306
  • Jackson, D., (2006) Software Abstractions, , MIT Press
  • Jackson, D., Vaziri, M., Finding bugs with a constraint solver (2000) ISSTA'00, pp. 14-25
  • Khurshid, S., Marinov, D., Jackson, D., An analyzable annotation language (2002) OOPSLA, pp. 231-245
  • Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D., A case for efficient solution enumeration SAT 2003, LNCS 2919, pp. 272-286
  • Ma, Y.-S., Offutt, J., Kwon, Y.-R., MuJava: An automated class mutation system (2005) Journal of Software Testing, Verification and Reliability, 15 (2), pp. 97-133
  • Musuvathi, M., Dill, D.L., An incremental heap canonicalization algorithm SPIN 2005, pp. 28-42
  • Rugina, R., Rinard, M.C., Symbolic bounds analysis of pointers, array indices, and accessed memory regions (2000) PLDI 2000, pp. 182-195
  • Sagiv, S., Reps, T.W., Wilhelm, R., Parametric shape analysis via 3-valued logic (2002) ACM TOPLAS, 24 (3), pp. 217-298
  • Siddiqui, J.H., Khurshid, S., An empirical study of structural constraint solving techniques (2009) ICFEM 2009, LNCS 5885, pp. 88-106
  • Torlak, E., Jackson, D., Kodkod: A relational model finder TACAS '07, LNCS 4425, pp. 632-647
  • Vaziri, M., Jackson, D., Checking properties of heap-manipulating procedures with a constraint solver TACAS 2003, pp. 505-520
  • Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F., Model checking programs (2003) ASE Journal, 10 (2)
  • 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
  • Visser, W., (2010) Private Communication, , February 2nd
  • Xie, Y., Aiken, A., Saturn: A scalable framework for error detection using boolean satisfiability (2007) ACM TOPLAS, 29 (3)A4 - ACM SIGSOFT

Citas:

---------- APA ----------
Galeotti, J.P., Rosner, N., Pombo, C.G.L. & Frias, M.F. (2010) . Analysis of invariants for efficient bounded verification. 19th International Symposium on Software Testing and Analysis, ISSTA 2010, 25-35.
http://dx.doi.org/10.1145/1831708.1831712
---------- CHICAGO ----------
Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F. "Analysis of invariants for efficient bounded verification" . 19th International Symposium on Software Testing and Analysis, ISSTA 2010 (2010) : 25-35.
http://dx.doi.org/10.1145/1831708.1831712
---------- MLA ----------
Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F. "Analysis of invariants for efficient bounded verification" . 19th International Symposium on Software Testing and Analysis, ISSTA 2010, 2010, pp. 25-35.
http://dx.doi.org/10.1145/1831708.1831712
---------- VANCOUVER ----------
Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F. Analysis of invariants for efficient bounded verification. ISSTA - Proc. Int. Symp. Softw. Test. Anal. 2010:25-35.
http://dx.doi.org/10.1145/1831708.1831712