Skip to main content
Top

2017 | OriginalPaper | Chapter

On the Completeness of Selective Unification in Concolic Testing of Logic Programs

Authors : Fred Mesnard, Étienne Payet, Germán Vidal

Published in: Logic-Based Program Synthesis and Transformation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Concolic testing is a popular dynamic validation technique that can be used for both model checking and automatic test case generation. We have recently introduced concolic testing in the context of logic programming. In contrast to previous approaches, the key ingredient in this setting is a technique to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. This is called “selective” unification. In this paper, we show that the existing algorithm is not complete and explore different alternatives in order to have a sound and complete algorithm for selective unification.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
Following the linear semantics of [12], we consider sequences of goals to represent the leaves of the SLD tree built so far.
 
Literature
1.
go back to reference Anand, S., Pasareanu, C.S., Visser, W.: Symbolic execution with abstraction. STTT 11(1), 53–67 (2009)CrossRef Anand, S., Pasareanu, C.S., Visser, W.: Symbolic execution with abstraction. STTT 11(1), 53–67 (2009)CrossRef
2.
go back to reference Apt, K.R.: From Logic Programming to Prolog. Prentice Hall, Englewood Cliffs (1997) Apt, K.R.: From Logic Programming to Prolog. Prentice Hall, Englewood Cliffs (1997)
3.
go back to reference Clarke, L.A.: A program testing system. In: Proceedings of the 1976 Annual Conference (ACM 1976), pp. 488–491 (1976) Clarke, L.A.: A program testing system. In: Proceedings of the 1976 Annual Conference (ACM 1976), pp. 488–491 (1976)
4.
go back to reference Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI 2005, pp. 213–223. ACM (2005) Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of PLDI 2005, pp. 213–223. ACM (2005)
5.
go back to reference Godefroid, P., Levin, M.Y., Molnar, D.A.: Sage: whitebox fuzzing for security testing. CACM 55(3), 40–44 (2012)CrossRef Godefroid, P., Levin, M.Y., Molnar, D.A.: Sage: whitebox fuzzing for security testing. CACM 55(3), 40–44 (2012)CrossRef
7.
go back to reference Mesnard, F., Payet, É., Vidal, G.: Concolic testing in logic programming. TPLP 15(4–5), 711–725 (2015)MathSciNet Mesnard, F., Payet, É., Vidal, G.: Concolic testing in logic programming. TPLP 15(4–5), 711–725 (2015)MathSciNet
9.
go back to reference Palamidessi, C.: Algebraic properties of idempotent substitutions. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 386–399. Springer, Heidelberg (1990). doi:10.1007/BFb0032046 CrossRef Palamidessi, C.: Algebraic properties of idempotent substitutions. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 386–399. Springer, Heidelberg (1990). doi:10.​1007/​BFb0032046 CrossRef
10.
go back to reference Pasareanu, C.S., Rungta, N., PathFinder, S.: symbolic execution of Java bytecode. In: Pecheur, C., Andrews, J., Nitto, E.D. (eds.) ASE, pp. 179–180. ACM (2010) Pasareanu, C.S., Rungta, N., PathFinder, S.: symbolic execution of Java bytecode. In: Pecheur, C., Andrews, J., Nitto, E.D. (eds.) ASE, pp. 179–180. ACM (2010)
11.
go back to reference 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) 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)
12.
go back to reference Ströder, T., Emmes, F., Schneider-Kamp, P., Giesl, J., Fuhs, C.: A linear operational semantics for termination and complexity analysis of ISO Prolog. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 237–252. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32211-2_16 CrossRef Ströder, T., Emmes, F., Schneider-Kamp, P., Giesl, J., Fuhs, C.: A linear operational semantics for termination and complexity analysis of ISO Prolog. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 237–252. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-32211-2_​16 CrossRef
Metadata
Title
On the Completeness of Selective Unification in Concolic Testing of Logic Programs
Authors
Fred Mesnard
Étienne Payet
Germán Vidal
Copyright Year
2017
DOI
https://doi.org/10.1007/978-3-319-63139-4_12

Premium Partner