Concolic Execution in Functional Programming by Program Instrumentation

  • Adrián Palacios
  • Germán VidalEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9527)


Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augmented in order to also deal with symbolic values. In this paper, in contrast, we present an alternative approach that is based on a program instrumentation. Basically, the execution of the instrumented program in a standard environment produces a sequence of events that can be used to reconstruct the associated symbolic execution.



We thank the anonymous reviewers and the participants of LOPSTR 2015 for their useful comments to improve this paper.


  1. 1.
    Armstrong, J., Virding, R., Williams, M.: Concurrent programming in ERLANG. Prentice Hall, Englewood Cliffs (1993)zbMATHGoogle Scholar
  2. 2.
    Carlsson, R.: An Introduction to Core Erlang. In: Proceedings of the PLI 2001 Erlang Workshop (2001).
  3. 3.
    Giantsios, A., Papaspyrou, N.S., Sagonas, K.F.: Concolic testing for functional languages. In: Proceedings of PPDP 2015, pp. 137–148. ACM (2015)Google Scholar
  4. 4.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI 2005, pp. 213–223. ACM (2005)Google Scholar
  5. 5.
    Godefroid, P., Levin, M.Y., Molnar, D.A.: Sage: whitebox fuzzing for security testing. Commun. ACM 55(3), 40–44 (2012)CrossRefGoogle Scholar
  6. 6.
    Gotovos, A., Christakis, M., Sagonas, K.F.: Test-driven development of concurrent programs using Concuerror. In: Rikitake, K., Stenman, E. (eds.), Proceedings of the 10th ACM SIGPLAN Workshop on Erlang, pp. 51–61. ACM (2011)Google Scholar
  7. 7.
    Kahn, G.: Natural semantics. In: Brandenburg, F.-J., Vidal-Naquet, G., Wirsing, M. (eds.), Proceedings of STACS 1987, pp. 22–39 (1987)Google Scholar
  8. 8.
    King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Mesnard, F., Payet, E., Vidal, G.: Concolic testing in logic programming. Theor. Pract. Logic Program. 15, 711–725 (2015)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Pasareanu, C.S., Rungta, N.: Symbolic PathFinder: symbolic execution of Java bytecode. In: Pecheur, C., Andrews, J., Di Nitto, E. (eds.), ASE, pp. 179–180. ACM (2010)Google Scholar
  11. 11.
    Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC/SIGSOFT FSE 2005, pp. 263–272. ACM (2005)Google Scholar
  12. 12.
    Vidal, G.: Towards symbolic execution in Erlang. In: Voronkov, A., Virbitskaite, I. (eds.) PSI 2014. LNCS, vol. 8974, pp. 351–360. Springer, Heidelberg (2015) Google Scholar
  13. 13.
    Vidal, G.: Concolic execution and test case generation in Prolog. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 167–181. Springer, Heidelberg (2015) Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.MiST, DSICUniversitat Politècnica de ValènciaValenciaSpain

Personalised recommendations