Automated Workarounds from Java Program Specifications Based on SAT Solving

  • Marcelo UvaEmail author
  • Pablo Ponzio
  • Germán Regis
  • Nazareno Aguirre
  • Marcelo F. Frias
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10202)


The failures that bugs in software lead to can sometimes be bypassed by the so called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Previous works have exploited this workarounds notion to automatically recover from runtime failures in some application domains. However, existing approaches that compute workarounds automatically either require the user to manually build an abstract model of the software under consideration, or to provide equivalent sequences of operations from which workarounds are computed, diminishing the automation of workaround-based system recovery.

In this paper, we present two techniques that automatically compute workarounds from Java code equipped with formal specifications, avoiding abstract software models and user provided equivalences. These techniques employ SAT solving to compute workarounds on concrete program state characterizations. The first employs SAT solving to compute traditional workarounds, while the second directly exploits SAT solving to circumvent a failing method, building a state that mimics the (correct) behaviour of this failing routine. Our experiments, based on case studies involving implementations of collections and a library for date arithmetic, enable us to show that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in time that makes them feasible to be used for run time repairs.


  1. 1.
    Replication package for Automated Workarounds from Java Program Specifications based on SAT Solving.
  2. 2.
    Abad, P., Aguirre, N., Bengolea, V., Ciolek, D., Frias, M., Galeotti, J., Maibaum, T., Moscato, M., Rosner, N., Vissani, I.: Improving test generation under rich contracts by tight bounds and incremental SAT solving. In: Proceedings of 6th IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg City, Luxembourg. IEEE (2013)Google Scholar
  3. 3.
    Belt, J., Robby, Deng, X.: Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses. In: Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and The ACM SIGSOFT International Symposium on Foundations of Software Engineering ESEC/FSE 2009. ACM (2009)Google Scholar
  4. 4.
    Carzaniga, A., Gorla, A., Pezzè, M.: Self-healing by means of automatic workarounds. In: Proceedings of 2008 ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2008, Leipzig, Germany, 12–13 May. ACM (2008)Google Scholar
  5. 5.
    Carzaniga, A., Gorla, A., Perino, N., Pezzè, M.: Automatic workarounds for web applications. In: Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2010, Santa Fe (NM), USA. ACM (2010)Google Scholar
  6. 6.
    Carzaniga, A., Gorla, A., Perino, N., Pezzè, M.: RAW: runtime automatic workarounds. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, ICSE 2010. ACM, New York (2010)Google Scholar
  7. 7.
    Carzaniga, A., Gorla, A., Mattavelli, A., Perino, N., Pezzè, M.: Automatic recovery from runtime failures. In: Proceedings of the 35th International Conference on Software Engineering ICSE 2013. IEEE/ACM, San Francisco (2013)Google Scholar
  8. 8.
    Carzaniga, A., Gorla, A., Perino, N., Pezzè, M.: Automatic workarounds: exploiting the intrinsic redundancy of web applications. ACM Trans. Softw. Eng. Methodol. 24(3) (2015). ACMGoogle Scholar
  9. 9.
    Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC/Java2. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006). doi: 10.1007/11804192_16 CrossRefGoogle Scholar
  10. 10.
    Debroy, V., Wong, W.E.: Using mutation to automatically suggest fixes to faulty programs. In: ICST 2010, pp. 65–74 (2010)Google Scholar
  11. 11.
    Demsky, B., Rinard, M.: Static specification analysis for termination of specification-based data structure repair. In: Proceedings of the 2003 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2003. ACM (2003)Google Scholar
  12. 12.
    Frias, M., Galeotti, J., López Pombo, C., Aguirre, N.: DynAlloy: upgrading alloy with actions. In: Proceedings of International Conference on Software Engineering, ICSE 2005, St. Louis, Missouri, USA. ACM (2005)Google Scholar
  13. 13.
    Galeotti, J.P., Frias, M.F.: DynAlloy as a formal method for the analysis of Java programs. In: Sacha, K. (ed.) Software Engineering Techniques: Design for Quality. IFIP, vol. 227, pp. 249–260. Springer, Boston (2006). doi: 10.1007/978-0-387-39388-9_24 CrossRefGoogle Scholar
  14. 14.
    Galeotti, J.P., Rosner, N., López Pombo, C., Frias, M.: Analysis of invariants for efficient bounded verification. In: Proceedings of the Nineteenth International Symposium on Software Testing and Analysis, ISSTA 2010, Trento, Italy, 12–16 July. ACM (2010)Google Scholar
  15. 15.
    Galeotti, J.P., Rosner, N., López Pombo, C., Frias, M.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Softw. Eng. 39(9), 1283–1307 (2013). IEEECrossRefGoogle Scholar
  16. 16.
    Geldenhuys, J., Aguirre, N., Frias, M.F., Visser, W.: Bounded lazy initialization. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 229–243. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38088-4_16 CrossRefGoogle Scholar
  17. 17.
    Hussain, I., Csallner, C.: Dynamic symbolic data structure repair. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, ICSE 2010. ACM (2010)Google Scholar
  18. 18.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)Google Scholar
  19. 19.
    Khurshid, S., García, I., Suen, Y.L.: Repairing structurally complex data. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 123–138. Springer, Heidelberg (2005). doi: 10.1007/11537328_12 CrossRefGoogle Scholar
  20. 20.
    Kim, D., Nam, J., Song, J., Kim, S.: Automatic patch generation learned from human-written patches. In: ICSE 2013, pp. 802–811 (2013)Google Scholar
  21. 21.
    Liskov, B., Guttag, J.: Program Development in Java: Abstraction, Specification and Object-Oriented Design. Addison-Wesley, Boston (2000)zbMATHGoogle Scholar
  22. 22.
    Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: Proceedings of International Conference on Software Engineering, ICSE 2007. IEEE (2007)Google Scholar
  23. 23.
    Qi, Z., Long, F., Achour, S., Rinard, M.C.: An analysis of patch plausibility and correctness for generate-and-validate patch generation systems. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, Baltimore, MD, USA, 12–17 July 2015, pp. 24–36 (2015)Google Scholar
  24. 24.
    Rosner, N., Bengolea, V., Ponzio, P., Khalek, S., Aguirre, N., Frias, M., Khurshid, S.: Bounded Exhaustive test input generation from hybrid invariants. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014. ACM (2014)Google Scholar
  25. 25.
    Rosner, N., Geldenhuys, J., Aguirre, N., Visser, W., Frias, M.: BLISS: improved symbolic execution by bounded lazy initialization with SAT support. IEEE Trans. Softw. Eng. 41(7), 639–660 (2015). IEEEGoogle Scholar
  26. 26.
    Samimi, H., Aung, E.D., Millstein, T.: Falling back on executable specifications. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 552–576. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14107-2_26 CrossRefGoogle Scholar
  27. 27.
    Smith, E.K., Barr, E., Le Goues, C., Brun, Y.: Is the cure worse than the disease? overfitting in automated program repair. In: Symposium on the Foundations of Software Engineering (FSE) (2015)Google Scholar
  28. 28.
    Visser, W., Pasareanu, C., Pelánek, R.: Test input generation for java containers using state matching. In: Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006. ACM (2006)Google Scholar
  29. 29.
    Weimer, W., Nguyen, T., Le Goues, C., Forrest, S.: Automatically finding patches using genetic programming. In: ICSE 2009, pp. 364–374 (2009)Google Scholar
  30. 30.
    Nokhbeh Zaeem, R., Khurshid, S.: Contract-based data structure repair using alloy. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 577–598. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14107-2_27 CrossRefGoogle Scholar
  31. 31.
    Nokhbeh Zaeem, R., Gopinath, D., Khurshid, S., McKinley, K.S.: History-aware data structure repair using SAT. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 2–17. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28756-5_2 CrossRefGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  • Marcelo Uva
    • 1
    Email author
  • Pablo Ponzio
    • 1
    • 3
  • Germán Regis
    • 1
  • Nazareno Aguirre
    • 1
    • 3
  • Marcelo F. Frias
    • 2
    • 3
  1. 1.Universidad Nacional de Río CuartoRío CuartoArgentina
  2. 2.Instituto Tecnológico de Buenos Aires (ITBA)Buenos AiresArgentina
  3. 3.Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET)Buenos AiresArgentina

Personalised recommendations