Navegar

Colección

Datos Estadísticas

Conferencia

Rosner, N.; Galeotti, J.; Bermúdez, S.; Blas, G.M.; De Rosso, S.P.; Pizzagalli, L.; Zemín, L.; Frias, M.F. "Parallel bounded analysis in code with rich invariants by refinement of field bounds" (2013) 22nd International Symposium on Software Testing and Analysis, ISSTA 2013:23-33
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor

Abstract:

In this article we present a novel technique for automated parallel bug-finding based on the sequential analysis tool TACO. TACO is a tool based on SAT-solving for efficient bug-finding in Java code with rich class invariants. It prunes the SAT-solver's search space by introducing precise symmetry-breaking predicates and bounding the relational semantics of Java class fields. The bounds computed by TACO generally include a substantial amount of nondeterminism; its reduction allows us to split the original analysis into disjoint subproblems. We discuss the soundness and completeness of the decomposition. Furthermore, we present experimental results showing that MUCHO-TACO, our tool which implements this technique, yields significant speed-ups over TACO on commodity cluster hardware. © 2013 ACM.

Registro:

Documento: Conferencia
Título:Parallel bounded analysis in code with rich invariants by refinement of field bounds
Autor:Rosner, N.; Galeotti, J.; Bermúdez, S.; Blas, G.M.; De Rosso, S.P.; Pizzagalli, L.; Zemín, L.; Frias, M.F.
Ciudad:Lugano
Filiación:FCEyN - UBA, Buenos Aires, Argentina
Saarland University, Saarbrücken, Germany
ITBA, Buenos Aires, Argentina
Palabras clave:Alloy; DynAlloy; SAT-based code analysis; Static analysis; Code analysis; Commodity clusters; DynAlloy; Novel techniques; Relational semantics; Sequential analysis; Soundness and completeness; Symmetry-breaking; Alloying; Cerium alloys; Software testing; Tools; Static analysis
Año:2013
Página de inicio:23
Página de fin:33
DOI: http://dx.doi.org/10.1145/2483760.2483770
Título revista:22nd International Symposium on Software Testing and Analysis, ISSTA 2013
Título revista abreviado:Int. Symp. Softw. Test. Anal., ISSTA - Proc.
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97814503_v_n_p23_Rosner

Referencias:

  • Abad, P., Aguirre, N., Bengolea, V., Ciolek, D., Frias, M.F., Galeotti, J., Maibaum, T., Vissani, I., Tight Bounds + Incremental SAT = Better Test Generation under Rich Contracts Proceedings of ICST 2013, , to appear in
  • Belt, J., Robby, Deng, X., Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analyses FSE 2009, pp. 355-364
  • Dolby, J., Vaziri, M., Tip, F., Finding Bugs Efficiently with a SAT Solver (2007) ESEC/FSE'07, pp. 195-204. , ACM Press
  • Bouillaguet, Ch., Kuncak, V., Wies, T., Zee, K., Rinard, M.C., Using First-Order Theorem Provers in the Jahob Data Structure Verification System VMCAI 2007, pp. 74-88
  • Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on Java predicates ISSTA 2002, 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
  • Chrabakh, W., Wolski, R., GrADSAT: A Parallel SAT Solver for the Grid UCSB Computer Science Technical Report Number 2003-05
  • Cuervo-Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.F., A dataflow analysis to improve SAT-based program verification Proceedings of SEFM 2011, , to appear in
  • Deng, X., Robby, Hatcliff, J., Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs SEFM 2007, pp. 273-282
  • Dennis, G., Chang, F., Jackson, D., Modular Verification of Code with SAT (2006) ISSTA'06, pp. 109-120
  • Flanagan, C., Leino, R., Lillibridge, M., Nelson, G., Saxe, J., Stata, R., Extended static checking for Java PLDI 2002, pp. 234-245
  • Galeotti, J.P., Rosner, N., Pombo, C.L., Frias, M.F., Analysis of invariants for efficient bounded verification ISSTA 2010, pp. 25-36
  • Galeotti, J.P., Rosner, N., Pombo, C.L., Frias, M.F., TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds (2013) IEEE TSE, , submitted to
  • Gil, L., Flores, P., Silveira, L.M., PMSat: A parallel version of MiniSAT (2008) Journal on Satisfiability, Boolean Modeling and Computation, 6, pp. 71-98
  • Jackson, D., Schechter, I., Shlyakhter, I., Alcoa: The alloy constraint analyzer Proceedings of International Conference on Software Engineering, Limerick, Ireland, 2000
  • 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., TestEra: Specification-Based Testing of Java Programs Using SAT (2004) Automated Software Engineering, 11 (4), pp. 403-434
  • Leino, K.R.M., Specification and verification of Object-Oriented Software (2008) Lecture Notes from Marktoberdorf International Summer School
  • Ohmura, K., Ueda, K., c-sat: A Parallel SAT Solver for Clusters (2009) LNCS, 5585. , SAT 2009
  • Shao, D., Gopinath, D., Khurshid, S., Perry, D.E., Optimizing Incremental Scope-Bounded Checking with Data-Flow Analysis ISSRE 2010, pp. 408-417
  • Shao, D., Khurshid, S., Perry, D.E., An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method FM 2009, pp. 757-772
  • Sharma, R., Gligoric, M., Arcuri, A., Fraser, G., Marinov, D., Testing Container Classes: Random or Systematic? FASE 2011, pp. 262-277
  • Siddiqui, J.H., Khurshid, S., PKorat: Parallel Generation of Structurally Complex Test Inputs Proceedings of ICST'09
  • Staats, M., Pasareanu, C.S., Parallel symbolic execution for structural test generation ISSTA 2010, pp. 183-194
  • Torlak, E., Jackson, D., Kodkod: A Relational Model Finder LNCS, 4425, pp. 632-647. , TACAS '07
  • 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
  • Zhang, H., Bonacina, M.P., Hsiang, J., PSATO: A distributed propositional prover and its application to quasigroup problems (1996) J. Symb. Comput., 21, pp. 4-6. , June 1996
  • http://www.mfrias.com.ar/; http://cecar.fcen.uba.ar/A4 - ACM SIGSOFT; Universita della Svizzera Italiana, Faculty of Informatics; UBS; Hasler Foundation; Orange

Citas:

---------- APA ----------
Rosner, N., Galeotti, J., Bermúdez, S., Blas, G.M., De Rosso, S.P., Pizzagalli, L., Zemín, L.,..., Frias, M.F. (2013) . Parallel bounded analysis in code with rich invariants by refinement of field bounds. 22nd International Symposium on Software Testing and Analysis, ISSTA 2013, 23-33.
http://dx.doi.org/10.1145/2483760.2483770
---------- CHICAGO ----------
Rosner, N., Galeotti, J., Bermúdez, S., Blas, G.M., De Rosso, S.P., Pizzagalli, L., et al. "Parallel bounded analysis in code with rich invariants by refinement of field bounds" . 22nd International Symposium on Software Testing and Analysis, ISSTA 2013 (2013) : 23-33.
http://dx.doi.org/10.1145/2483760.2483770
---------- MLA ----------
Rosner, N., Galeotti, J., Bermúdez, S., Blas, G.M., De Rosso, S.P., Pizzagalli, L., et al. "Parallel bounded analysis in code with rich invariants by refinement of field bounds" . 22nd International Symposium on Software Testing and Analysis, ISSTA 2013, 2013, pp. 23-33.
http://dx.doi.org/10.1145/2483760.2483770
---------- VANCOUVER ----------
Rosner, N., Galeotti, J., Bermúdez, S., Blas, G.M., De Rosso, S.P., Pizzagalli, L., et al. Parallel bounded analysis in code with rich invariants by refinement of field bounds. Int. Symp. Softw. Test. Anal., ISSTA - Proc. 2013:23-33.
http://dx.doi.org/10.1145/2483760.2483770