Skip to main content
Erschienen in: International Journal on Software Tools for Technology Transfer 4/2019

30.01.2018 | Regular Paper

Fast detection of concurrency errors by state space traversal with randomization and early backtracking

verfasst von: Pavel Parízek, Ondřej Lhoták

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 4/2019

Einloggen

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

search-config
loading …

Abstract

State space traversal is a very popular approach to detect concurrency errors and test concurrent programs. However, it is not practically feasible for complex programs with many thread interleavings and a large state space. Many techniques explore only a part of the state space in order to find errors quickly—building upon the observation that errors can often be found in a particular small part of the state space. Great improvements in performance have been achieved also through randomization. In the context of this research direction, we present the DFS-RB algorithm that augments the standard algorithm for depth-first traversal with early backtracking. Specifically, it is possible to backtrack early from a state before all outgoing transitions have been explored. The DFS-RB algorithm is non-deterministic—it uses random numbers, together with values of several parameters, to determine when and how early backtracking takes place in the search. To evaluate DFS-RB, we performed a large experimental study with our prototype implementation in Java Pathfinder on several Java programs. The results show that DFS-RB achieves better performance in terms of speed and error detection than many state-of-the-art techniques for many benchmarks in our set. Nevertheless, it is difficult to find a single configuration of DFS-RB that works well for many different benchmarks. We designed a ranking algorithm whose purpose is to identify configurations that yield overall consistently good performance with a small variation.

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!

Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
We used the release of JPF corresponding to the commit number 715 in the repository for JPF v6.
 
2
We used the version defined by the commit number 29 in the repository that contains JPF v8.
 
Literatur
1.
Zurück zum Zitat Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of POPL. ACM (2014) Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of POPL. ACM (2014)
2.
Zurück zum Zitat Barnat, J., Brim, L., Rockai, P.: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. Sci. Comput. Program. 77(12), 1272–1288 (2012)CrossRefMATH Barnat, J., Brim, L., Rockai, P.: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. Sci. Comput. Program. 77(12), 1272–1288 (2012)CrossRefMATH
3.
Zurück zum Zitat Behrmann, G., Hune, T., Vaandrager, F.: Distributing timed model checking—how the search order matters. In: Proceedings of CAV, LNCS, vol. 1855 (2000) Behrmann, G., Hune, T., Vaandrager, F.: Distributing timed model checking—how the search order matters. In: Proceedings of CAV, LNCS, vol. 1855 (2000)
4.
Zurück zum Zitat Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. (JSAT) 4, 75–97 (2008)MATH Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. (JSAT) 4, 75–97 (2008)MATH
5.
Zurück zum Zitat Bisiani, R.: Beam Search. Encyclopedia of Artificial Intelligence. Wiley, New York (1992) Bisiani, R.: Beam Search. Encyclopedia of Artificial Intelligence. Wiley, New York (1992)
6.
Zurück zum Zitat Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A Randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of ASPLOS. ACM (2010) Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A Randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of ASPLOS. ACM (2010)
7.
Zurück zum Zitat Ciardo, G., Gluckman, J., Nicol, D.: Distributed state space generation of discrete-state stochastic models. INFORMS J. Comput. 10(1), 82–93 (1998)CrossRef Ciardo, G., Gluckman, J., Nicol, D.: Distributed state space generation of discrete-state stochastic models. INFORMS J. Comput. 10(1), 82–93 (1998)CrossRef
8.
Zurück zum Zitat Coons, K.E., Burckhardt, S., Musuvathi, M.: GAMBIT: effective unit testing for concurrency libraries. In: Proceedings of PPoPP. ACM (2010) Coons, K.E., Burckhardt, S., Musuvathi, M.: GAMBIT: effective unit testing for concurrency libraries. In: Proceedings of PPoPP. ACM (2010)
9.
Zurück zum Zitat Dwyer, M.B., Elbaum, S.G., Person, S., Purandare, R.: Parallel randomized state-space search. In: Proceedings of ICSE, IEEE CS (2007) Dwyer, M.B., Elbaum, S.G., Person, S., Purandare, R.: Parallel randomized state-space search. In: Proceedings of ICSE, IEEE CS (2007)
10.
Zurück zum Zitat Dwyer, M., Hatcliff, J., Robby, Ranganath, V.: Exploiting object escape and locking information in artial-order reductions for concurrent object-oriented programs. Formal Methods Syst. Des. 25(2–3), 199–240 (2004)CrossRefMATH Dwyer, M., Hatcliff, J., Robby, Ranganath, V.: Exploiting object escape and locking information in artial-order reductions for concurrent object-oriented programs. Formal Methods Syst. Des. 25(2–3), 199–240 (2004)CrossRefMATH
11.
Zurück zum Zitat Dwyer, M.B., Person, S., Elbaum, S.G.: Controlling factors in evaluating path-sensitive error detection techniques. In: Proceedings of SIGSOFT FSE. ACM (2006) Dwyer, M.B., Person, S., Elbaum, S.G.: Controlling factors in evaluating path-sensitive error detection techniques. In: Proceedings of SIGSOFT FSE. ACM (2006)
12.
Zurück zum Zitat Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Int. J. Softw. Tools Technol. Transf. 5(2–3), 247–267 (2004)CrossRefMATH Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Int. J. Softw. Tools Technol. Transf. 5(2–3), 247–267 (2004)CrossRefMATH
13.
Zurück zum Zitat Edelkamp, S., Schuppan, V., Bosnacki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Proceedings of 5th International Workshop on Model Checking and Artificial Intelligence, LNCS, vol. 5348 (2008) Edelkamp, S., Schuppan, V., Bosnacki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Proceedings of 5th International Workshop on Model Checking and Artificial Intelligence, LNCS, vol. 5348 (2008)
14.
Zurück zum Zitat Een, N., Sorensson, N.: An extensible SAT-solver. In: Proceedings of SAT, LNCS, vol. 2919 (2003) Een, N., Sorensson, N.: An extensible SAT-solver. In: Proceedings of SAT, LNCS, vol. 2919 (2003)
15.
Zurück zum Zitat Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Proceedings of POPL. ACM (2011) Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Proceedings of POPL. ACM (2011)
16.
Zurück zum Zitat Engels, T.A.N., Groote, J.F., van Weerdenburg, M.J., Willemse, T.A.C.: Search algorithms for automated validation. J. Logic Algebr. Program. 78(4), 274–287 (2009)MathSciNetCrossRefMATH Engels, T.A.N., Groote, J.F., van Weerdenburg, M.J., Willemse, T.A.C.: Search algorithms for automated validation. J. Logic Algebr. Program. 78(4), 274–287 (2009)MathSciNetCrossRefMATH
17.
Zurück zum Zitat Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: Proceedings of ESEC/FSE. ACM (2013) Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: Proceedings of ESEC/FSE. ACM (2013)
18.
Zurück zum Zitat Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL. ACM (2005) Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL. ACM (2005)
19.
Zurück zum Zitat Godefroid, P.: Partial-order methods for the verification of concurrent systems. In: LNCS, vol. 1032 (1996) Godefroid, P.: Partial-order methods for the verification of concurrent systems. In: LNCS, vol. 1032 (1996)
20.
Zurück zum Zitat Gomes, C., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI (1998) Gomes, C., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI (1998)
21.
Zurück zum Zitat Groce, A., Visser, W.: Heuristics for model checking Java programs. Int. J. Softw. Tools Technol. Transf. 6(4), 260–276 (2004)CrossRefMATH Groce, A., Visser, W.: Heuristics for model checking Java programs. Int. J. Softw. Tools Technol. Transf. 6(4), 260–276 (2004)CrossRefMATH
22.
Zurück zum Zitat Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Proceedings of SPIN, LNCS, vol. 4595 (2007) Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Proceedings of SPIN, LNCS, vol. 4595 (2007)
23.
Zurück zum Zitat Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659–674 (2007)CrossRef Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659–674 (2007)CrossRef
24.
Zurück zum Zitat Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Proceedings of SPIN, LNCS, vol. 5156 (2008) Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Proceedings of SPIN, LNCS, vol. 5156 (2008)
25.
Zurück zum Zitat Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of ASE, IEEE CS (2008) Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of ASE, IEEE CS (2008)
26.
Zurück zum Zitat Jagannath, V., Kirn, M., Lin, Y., Marinov, D.: Evaluating machine-independent metrics for state-space exploration. In: Proceedings of ICST, IEEE CS (2012) Jagannath, V., Kirn, M., Lin, Y., Marinov, D.: Evaluating machine-independent metrics for state-space exploration. In: Proceedings of ICST, IEEE CS (2012)
27.
Zurück zum Zitat Jones, M., Mercer, E.: Explicit state model checking with hopper. In: Proceedings of SPIN, LNCS, vol. 2989 (2004) Jones, M., Mercer, E.: Explicit state model checking with hopper. In: Proceedings of SPIN, LNCS, vol. 2989 (2004)
28.
Zurück zum Zitat Jones, M., Sorber, J.: Parallel search for LTL violations. Int. J. Softw. Tools Technol. Transf. 7(1), 31–42 (2005)CrossRef Jones, M., Sorber, J.: Parallel search for LTL violations. Int. J. Softw. Tools Technol. Transf. 7(1), 31–42 (2005)CrossRef
29.
Zurück zum Zitat Kalibera, T., Hagelberg, J., Pizlo, F., Plsek, A., Titzer, B., Vitek, J.: CDx: a family of real-time Java benchmarks. In: Proceedings of JTRES. ACM (2009) Kalibera, T., Hagelberg, J., Pizlo, F., Plsek, A., Titzer, B., Vitek, J.: CDx: a family of real-time Java benchmarks. In: Proceedings of JTRES. ACM (2009)
30.
Zurück zum Zitat Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Proceedings of ATVA, LNCS, vol. 6996 (2011) Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Proceedings of ATVA, LNCS, vol. 6996 (2011)
31.
Zurück zum Zitat Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Proceedings of FMCAD. IEEE (2010) Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Proceedings of FMCAD. IEEE (2010)
32.
Zurück zum Zitat Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Proceedings of SPIN, LNCS, vol. 1680 (1999) Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Proceedings of SPIN, LNCS, vol. 1680 (1999)
33.
34.
Zurück zum Zitat van Moorsel, A.P.A., Wolter, K.: Analysis of restart mechanisms in software systems. IEEE Trans. Softw. Eng. 32(8), 547–558 (2006)CrossRef van Moorsel, A.P.A., Wolter, K.: Analysis of restart mechanisms in software systems. IEEE Trans. Softw. Eng. 32(8), 547–558 (2006)CrossRef
35.
Zurück zum Zitat Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of PLDI. ACM (2007) Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of PLDI. ACM (2007)
36.
Zurück zum Zitat Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of OSDI, USENIX (2008) Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of OSDI, USENIX (2008)
37.
Zurück zum Zitat Parízek, P., Kalibera, T.: Efficient detection of errors in Java components using random environment and restarts. In: Proceedings of TACAS, LNCS, vol. 6015 (2010) Parízek, P., Kalibera, T.: Efficient detection of errors in Java components using random environment and restarts. In: Proceedings of TACAS, LNCS, vol. 6015 (2010)
38.
Zurück zum Zitat Parízek, P., Lhoták, O.: Randomized backtracking in state space traversal. In: Proceedings of SPIN, LNCS, vol. 6823 (2011) Parízek, P., Lhoták, O.: Randomized backtracking in state space traversal. In: Proceedings of SPIN, LNCS, vol. 6823 (2011)
39.
Zurück zum Zitat Parízek, P., Lhoták, O.: Identifying future field accesses in exhaustive state space traversal. In: Proceedings of ASE, IEEE CS (2011) Parízek, P., Lhoták, O.: Identifying future field accesses in exhaustive state space traversal. In: Proceedings of ASE, IEEE CS (2011)
40.
Zurück zum Zitat Parízek, P.: Hybrid analysis for partial order reduction of programs with arrays. In: Proceedings of VMCAI, LNCS, vol. 9583 (2016) Parízek, P.: Hybrid analysis for partial order reduction of programs with arrays. In: Proceedings of VMCAI, LNCS, vol. 9583 (2016)
41.
Zurück zum Zitat Parízek, P.: Fast error detection with hybrid analyses of future accesses. In: Proceedings of SAC, MUSEPAT Track. ACM (2016) Parízek, P.: Fast error detection with hybrid analyses of future accesses. In: Proceedings of SAC, MUSEPAT Track. ACM (2016)
42.
Zurück zum Zitat Qadeer, S.: Daisy File System. Joint CAV/ISSTA special event on specification, verification and testing of concurrent software (2004) Qadeer, S.: Daisy File System. Joint CAV/ISSTA special event on specification, verification and testing of concurrent software (2004)
43.
Zurück zum Zitat Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS, LNCS, vol. 3440 (2005) Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS, LNCS, vol. 3440 (2005)
44.
Zurück zum Zitat Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Proceedings of CAV, LNCS, vol. 3576 (2005) Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Proceedings of CAV, LNCS, vol. 3576 (2005)
45.
Zurück zum Zitat Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized Büchi automata. In: Proceedings of TACAS, LNCS, vol. 9035 (2015) Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized Büchi automata. In: Proceedings of TACAS, LNCS, vol. 9035 (2015)
46.
Zurück zum Zitat Rungta, N., Mercer, E.: Generating counter-examples through randomized guided search. In: Proceedings of SPIN, LNCS, vol. 4595 (2007) Rungta, N., Mercer, E.: Generating counter-examples through randomized guided search. In: Proceedings of SPIN, LNCS, vol. 4595 (2007)
47.
Zurück zum Zitat Rungta, N., Mercer, E.: Clash of the titans: tools and techniques for hunting bugs in concurrent programs. In: Proceedings of PADTAD. ACM (2009) Rungta, N., Mercer, E.: Clash of the titans: tools and techniques for hunting bugs in concurrent programs. In: Proceedings of PADTAD. ACM (2009)
48.
Zurück zum Zitat Sen, K.: Effective random testing of concurrent programs. In: Proceedings of ASE. ACM (2007) Sen, K.: Effective random testing of concurrent programs. In: Proceedings of ASE. ACM (2007)
49.
Zurück zum Zitat Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae 70(1–2), 111–126 (2006)MathSciNetMATH Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae 70(1–2), 111–126 (2006)MathSciNetMATH
51.
Zurück zum Zitat Spearman, C.: The proof and measurement of association between two things. Am. J. Psychol. 15(1), 72–101 (1904)CrossRef Spearman, C.: The proof and measurement of association between two things. Am. J. Psychol. 15(1), 72–101 (1904)CrossRef
52.
Zurück zum Zitat Stern, U., Dill, D.L.: Parallelizing the murphi verifier. In: Proceedings of CAV, LNCS, vol. 1254 (1997) Stern, U., Dill, D.L.: Parallelizing the murphi verifier. In: Proceedings of CAV, LNCS, vol. 1254 (1997)
53.
Zurück zum Zitat Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: Proceedings of PPoPP. ACM (2014) Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: Proceedings of PPoPP. ACM (2014)
54.
Zurück zum Zitat Udupa, A., Desai, A., Rajamani, S.: Depth bounded explicit-state model checking. In: Proceedings of SPIN, LNCS, vol. 6823 (2011) Udupa, A., Desai, A., Rajamani, S.: Depth bounded explicit-state model checking. In: Proceedings of SPIN, LNCS, vol. 6823 (2011)
55.
Zurück zum Zitat Vargha, A., Delaney, H.D.: A critique and improvement of the CL common language effect size statistics of McGraw and Wong. J. Educ. Behav. Stat. 25(2), 101–132 (2000) Vargha, A., Delaney, H.D.: A critique and improvement of the CL common language effect size statistics of McGraw and Wong. J. Educ. Behav. Stat. 25(2), 101–132 (2000)
56.
Zurück zum Zitat Walsh, T.: Search in a small world. In: Proceedings of IJCAI, Morgan Kaufmann (1999) Walsh, T.: Search in a small world. In: Proceedings of IJCAI, Morgan Kaufmann (1999)
57.
Zurück zum Zitat Wehrle, M., Kupferschmid, S., Podelski, A.: Transition-based directed model checking. In: Proceedings of TACAS, LNCS, vol. 5505 (2009) Wehrle, M., Kupferschmid, S., Podelski, A.: Transition-based directed model checking. In: Proceedings of TACAS, LNCS, vol. 5505 (2009)
58.
Zurück zum Zitat Wehrle, M., Kupferschmid, S.: Context-enhanced directed model checking. In: Proceedings of SPIN, LNCS, vol. 6349 (2010) Wehrle, M., Kupferschmid, S.: Context-enhanced directed model checking. In: Proceedings of SPIN, LNCS, vol. 6349 (2010)
59.
Zurück zum Zitat Wijs, A., Bosnacki, D.: Many-core on-the-fly model checking of safety properties using GPUs. Int. J. Softw. Tools Technol. Transf. 18(2), 169–185 (2016)CrossRef Wijs, A., Bosnacki, D.: Many-core on-the-fly model checking of safety properties using GPUs. Int. J. Softw. Tools Technol. Transf. 18(2), 169–185 (2016)CrossRef
60.
Zurück zum Zitat Wijs, A., Lisser, B.: Distributed extended beam search for quantitative model checking. In: Proceedings of MoChArt, LNCS, vol. 4428 (2006) Wijs, A., Lisser, B.: Distributed extended beam search for quantitative model checking. In: Proceedings of MoChArt, LNCS, vol. 4428 (2006)
61.
Zurück zum Zitat Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: a runtime model checker for multithreaded C programs. Technical Report UUCS-08-004, University of Utah (2008) Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: a runtime model checker for multithreaded C programs. Technical Report UUCS-08-004, University of Utah (2008)
Metadaten
Titel
Fast detection of concurrency errors by state space traversal with randomization and early backtracking
verfasst von
Pavel Parízek
Ondřej Lhoták
Publikationsdatum
30.01.2018
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 4/2019
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-018-0484-7

Weitere Artikel der Ausgabe 4/2019

International Journal on Software Tools for Technology Transfer 4/2019 Zur Ausgabe