Skip to main content

2017 | OriginalPaper | Buchkapitel

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

verfasst von : Fred Mesnard, Étienne Payet, Germán Vidal

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Fußnoten
1
Following the linear semantics of [12], we consider sequences of goals to represent the leaves of the SLD tree built so far.
 
Literatur
1.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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
Metadaten
Titel
On the Completeness of Selective Unification in Concolic Testing of Logic Programs
verfasst von
Fred Mesnard
Étienne Payet
Germán Vidal
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-63139-4_12