Analysis of invariants for efficient bounded verification
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 inv...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2010
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 08619caa a22010457a 4500 | ||
|---|---|---|---|
| 001 | PAPER-7693 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203727.0 | ||
| 008 | 190411s2010 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-77955877107 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Galeotti, J.P. | |
| 245 | 1 | 0 | |a Analysis of invariants for efficient bounded verification |
| 260 | |c 2010 | ||
| 270 | 1 | 0 | |m Galeotti, J. P.; Department of Computer Science, FCEyN Universidad de Buenos AiresArgentina; email: jgaleotti@dc.uba.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D., Evaluating the "Small Scope Hypothesis", , http://sdg.csail.mit.edu/publications.html, downloadable from | ||
| 504 | |a Belt, J., Robby, Deng, X., Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-Based Analyses, FSE 2009, pp. 355-364 | ||
| 504 | |a 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 | ||
| 504 | |a Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on java predicates (2002) ISSTA, pp. 123-133 | ||
| 504 | |a 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 | ||
| 504 | |a Clarke, E., Kroening, D., Lerda, F., A tool for checking ANSI-C programs TACAS 2004, LNCS 2988, pp. 168-176 | ||
| 504 | |a 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 | ||
| 504 | |a 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 | ||
| 504 | |a Dennis, G., Chang, F., Jackson, D., Modular verification of code with SAT (2006) ISSTA'06, pp. 109-120 | ||
| 504 | |a Dennis, G., Yessenov, K., Jackson, D., Bounded verification of voting software (2008) VSTTE 2008, , Toronto, Canada, October | ||
| 504 | |a Dolby, J., Vaziri, M., Tip, F., Finding bugs efficiently with a SAT solver (2007) ESEC/FSE'07, pp. 195-204. , ACM Press | ||
| 504 | |a Flanagan, C., Leino, R., Lillibridge, M., Nelson, G., Saxe, J., Stata, R., Extended static checking for java (2002) PLDI, pp. 234-245 | ||
| 504 | |a Frias, M.F., Galeotti, J.P., Lopez Pombo, C.G., Aguirre, N., DynAlloy: Upgrading alloy with actions (2005) ICSE'05, pp. 442-450 | ||
| 504 | |a Frias, M.F., Lopez Pombo, C.G., Galeotti, J.P., Aguirre, N., Efficient analysis of DynAlloy specifications (2007) ACM-TOSEM, 17 (1) | ||
| 504 | |a 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 | ||
| 504 | |a Iosif, R., Symmetry reduction criteria for software model checking SPIN 2002, pp. 22-41 | ||
| 504 | |a 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 | ||
| 504 | |a Jackson, D., (2006) Software Abstractions, , MIT Press | ||
| 504 | |a Jackson, D., Vaziri, M., Finding bugs with a constraint solver (2000) ISSTA'00, pp. 14-25 | ||
| 504 | |a Khurshid, S., Marinov, D., Jackson, D., An analyzable annotation language (2002) OOPSLA, pp. 231-245 | ||
| 504 | |a Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D., A case for efficient solution enumeration SAT 2003, LNCS 2919, pp. 272-286 | ||
| 504 | |a 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 | ||
| 504 | |a Musuvathi, M., Dill, D.L., An incremental heap canonicalization algorithm SPIN 2005, pp. 28-42 | ||
| 504 | |a Rugina, R., Rinard, M.C., Symbolic bounds analysis of pointers, array indices, and accessed memory regions (2000) PLDI 2000, pp. 182-195 | ||
| 504 | |a Sagiv, S., Reps, T.W., Wilhelm, R., Parametric shape analysis via 3-valued logic (2002) ACM TOPLAS, 24 (3), pp. 217-298 | ||
| 504 | |a Siddiqui, J.H., Khurshid, S., An empirical study of structural constraint solving techniques (2009) ICFEM 2009, LNCS 5885, pp. 88-106 | ||
| 504 | |a Torlak, E., Jackson, D., Kodkod: A relational model finder TACAS '07, LNCS 4425, pp. 632-647 | ||
| 504 | |a Vaziri, M., Jackson, D., Checking properties of heap-manipulating procedures with a constraint solver TACAS 2003, pp. 505-520 | ||
| 504 | |a Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F., Model checking programs (2003) ASE Journal, 10 (2) | ||
| 504 | |a 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 | ||
| 504 | |a Visser, W., (2010) Private Communication, , February 2nd | ||
| 504 | |a Xie, Y., Aiken, A., Saturn: A scalable framework for error detection using boolean satisfiability (2007) ACM TOPLAS, 29 (3)A4 - ACM SIGSOFT | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Department of Computer Science, FCEyN Universidad de Buenos Aires, Argentina | ||
| 593 | |a Department of Software Engineering, Buenos Aires Institute of Technology (ITBA), Argentina | ||
| 690 | 1 | 0 | |a ALLOY |
| 690 | 1 | 0 | |a DYNALLOY |
| 690 | 1 | 0 | |a KODKOD |
| 690 | 1 | 0 | |a SAT-BASED CODE ANALYSIS |
| 690 | 1 | 0 | |a STATIC ANALYSIS |
| 690 | 1 | 0 | |a AUTOMATED TECHNIQUES |
| 690 | 1 | 0 | |a CODE ANALYSIS |
| 690 | 1 | 0 | |a DYNALLOY |
| 690 | 1 | 0 | |a EXECUTION TRACE |
| 690 | 1 | 0 | |a KODKOD |
| 690 | 1 | 0 | |a LINKED DATA STRUCTURES |
| 690 | 1 | 0 | |a ORDERS OF MAGNITUDE |
| 690 | 1 | 0 | |a PROPOSITIONAL FORMULAS |
| 690 | 1 | 0 | |a PROPOSITIONAL VARIABLES |
| 690 | 1 | 0 | |a PROTOTYPE TOOLS |
| 690 | 1 | 0 | |a SAT SOLVERS |
| 690 | 1 | 0 | |a SAT-BASED BOUNDED VERIFICATION |
| 690 | 1 | 0 | |a SAT-SOLVING |
| 690 | 1 | 0 | |a SEQUENTIAL PROGRAMS |
| 690 | 1 | 0 | |a SYMMETRY-BREAKING |
| 690 | 1 | 0 | |a TIGHT BOUND |
| 690 | 1 | 0 | |a COMPUTER SOFTWARE SELECTION AND EVALUATION |
| 690 | 1 | 0 | |a DATA STRUCTURES |
| 690 | 1 | 0 | |a JAVA PROGRAMMING LANGUAGE |
| 690 | 1 | 0 | |a SOFTWARE TESTING |
| 690 | 1 | 0 | |a STATIC ANALYSIS |
| 690 | 1 | 0 | |a MODEL CHECKING |
| 700 | 1 | |a Rosner, N. | |
| 700 | 1 | |a Pombo, C.G.L. | |
| 700 | 1 | |a Frias, M.F. | |
| 711 | 2 | |c Trento |d 12 July 2010 through 16 July 2010 |g Código de la conferencia: 81475 | |
| 773 | 0 | |d 2010 |h pp. 25-35 |p ISSTA - Proc. Int. Symp. Softw. Test. Anal. |n ISSTA'10 - Proceedings of the 2010 International Symposium on Software Testing and Analysis |z 9781605588230 |t 19th International Symposium on Software Testing and Analysis, ISSTA 2010 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-77955877107&doi=10.1145%2f1831708.1831712&partnerID=40&md5=e05b878e6ac1c4c96e6a8e32dba2978b |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1145/1831708.1831712 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_97816055_v_n_p25_Galeotti |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97816055_v_n_p25_Galeotti |y Registro en la Biblioteca Digital |
| 961 | |a paper_97816055_v_n_p25_Galeotti |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/conferenceObject |a info:ar-repo/semantics/documento de conferencia |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 68646 | ||