Top

Software and Systems Modeling

14-03-2024 | Special Section Paper

A lightweight approach to nontermination inference using Constrained Horn Clauses

Authors: Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Published in: Software and Systems Modeling

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

search-config

AI-assisted search

Off

Abstract

Nontermination is an unwanted program property for some software systems, and a safety property for other systems. In either case, automated discovery of preconditions for nontermination is of interest. We introduce NtHorn, a fast lightweight nontermination analyser, which is able to deduce non-trivial sufficient conditions for nontermination. Using Constrained Horn Clauses (CHCs) as a vehicle, we show how established techniques for CHC program transformation and abstract interpretation can be exploited for the purpose of nontermination analysis. NtHorn is comparable in effectiveness to the state-of-the-art nontermination analysis tools, as measured on standard competition benchmark suites (consisting of integer manipulating programs), while typically solving problems faster by one order of magnitude.

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!

inform now

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!

inform now

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!

inform now

A comma to the right of the arrow in a CHC denotes conjunction, and conjunction binds tighter than the arrow.

We use \(\forall (\varphi )\) for the universal closure of formula \(\varphi \), that is, \(\forall V (\varphi )\), where V is the set of free variables in \(\varphi \).

Readers familiar with predicative programming a la Hehner [38], may prefer to rename \(\texttt{d}\) in \(c_1\) to \(\texttt{a}'\) (and similarly rewrite other clauses), to support the reading “value of \(\texttt{a}\) after the assignment”.

Available from https://github.com/bishoksan/NtHorn.git.

Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.: Proving non-termination. In: Necula, G.C., Wadler, P. (eds.) Proc. 35th ACM Symp. Principles of Programming Languages, pp. 147–158. ACM, New York (2008). https://doi.org/10.1145/1328438.1328459

Chen, H.Y., Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.W.: Proving nontermination via safety. In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 8413, pp. 156–171. Springer, Berlin Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_11

Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Progr. 13(2 &3), 103–179 (1992). https://doi.org/10.1016/0743-1066(92)90030-7MathSciNetCrossRef

Cousot, P.: Principles of abstract interpretation. MIT Press, Cambridge MA (2021)

Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving termination through conditional termination. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 10205, pp. 99–117. Springer, Berlin Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_6

Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) Computer-Aided Verification. LNCS, vol. 8559, pp. 797–813. Springer, Berlin Heidelberg (2014). https://doi.org/10.1007/978-3-319-08867-9_53

Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 1–55 (2014). https://doi.org/10.1145/2629488MathSciNetCrossRef

Giesl, J., et al: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning. LNCS, vol. 8562, pp. 184–191. Springer, Berlin Heidelberg (2014). https://doi.org/10.1007/978-3-319-08587-6_13

Howe, J.M., King, A., Lu, L.: Analysing logic programs by reasoning backwards. In: Bruynooghe, M., Lau, K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 152–188. Springer, Berlin Heidelberg (2004). https://doi.org/10.1007/978-3-540-25951-0_6

10.

Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) Verification, Model Checking and Abstract Interpretation. LNCS, vol. 4905, pp. 188–202. Springer, Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-78163-9_18

11.

Miné, A.: Inferring sufficient conditions with backward polyhedral under-approximations. Electron. Notes Theoret. Comput. Sci. 287, 89–100 (2012). https://doi.org/10.1016/j.entcs.2012.09.009CrossRef

12.

Bakhirkin, A., Berdine, J., Piterman, N.: Backward analysis via over-approximate abstraction and under-approximate subtraction of Horn clauses. In: Müller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 34–50. Springer, Berlin Heidelberg (2014). https://doi.org/10.1007/978-3-319-10936-7_3

13.

Kafle, B., Gallagher, J.P., Gange, G., Schachte, P., Søndergaard, H., Stuckey, P.J.: An iterative approach to precondition inference using constrained Horn clauses. Theory Pract. Logic Progr. 18, 553–570 (2018). https://doi.org/10.1017/S1471068418000091MathSciNetCrossRef

14.

Le, T.C., Qin, S., Chin, W.-N.: Termination and non-termination specification inference. In: Grove, D., Blackburn, S.M. (eds.) Proc. 36th ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 489–498. ACM, New York (2015). https://doi.org/10.1145/2737924.2737993

15.

Kafle, B., Gange, G., Schachte, P., Søndergaard, H., Stuckey, P.J.: Lightweight nontermination inference with CHCs. In: Calinescu, R., Păsăreanu, C.S. (eds.) Software Engineering and Formal Methods. LNCS, vol. 13085, pp. 383–402. Springer, Switzerland (2021). https://doi.org/10.1007/978-3-030-92124-8_22

16.

Chatterjee, K., Goharshady, E.K., Novotný, P., Žikelić, D.: Proving non-termination by program reversal. In: Freund, S.N., Yahav, E. (eds.) Proc. 42nd ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 1033–1048. ACM, New York (2021). https://doi.org/10.1145/3453483.3454093

17.

Cousot, P., Cousot, R., Fähndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking and Abstract Interpretation. LNCS, vol. 7737, pp. 128–148. Springer, Berlin Heidelberg (2013). https://doi.org/10.1007/978-3-642-35873-9_10

18.

Bakhirkin, A.: Recurrent sets for non-termination and safety of programs. PhD thesis, University of Leicester (2016)

19.

Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of Horn clauses. In: Ranzato, F. (ed.) Static Analysis. LNCS, vol. 10422, pp. 23–45. Springer, Berlin Heidelberg (2017). https://doi.org/10.1007/978-3-319-66706-5_2

20.

Seghir, M.N., Schrammel, P.: Necessary and sufficient preconditions via eager abstraction. In: Garrigue, J. (ed.) Proc. 12th Asian Symp. Programming Languages and Systems. LNCS, vol. 8858, pp. 236–254. Springer, Berlin Heidelberg (2014). https://doi.org/10.1007/978-3-319-12736-1_13

21.

Kafle, B., Gange, G., Stuckey, P.J., Schachte, P., Søndergaard, H.: Transformation-enabled precondition inference. Theory Pract. Logic Progr. 21(6), 700–716 (2021). https://doi.org/10.1017/S1471068421000272MathSciNetCrossRef

22.

Doménech, J.J., Gallagher, J.P., Genaim, S.: Control-flow refinement by partial evaluation, and its application to termination and cost analysis. Theory Pract. Logic Progr. 19(5–6), 990–1005 (2019). https://doi.org/10.1017/S1471068419000310MathSciNetCrossRef

23.

Gallagher, J.P.: Polyvariant program specialisation with property-based abstraction. In: Lisitsa, A., Nemytykh, A.P. (eds.) Proc. Seventh Int. Workshop on Verification and Program Transformation. EPTCS, vol. 299, pp. 34–48 (2019). https://doi.org/10.4204/EPTCS.299.6

24.

Kafle, B., Gallagher, J.P.: Constraint specialisation in Horn clause verification. Sci. Comput. Progr. 137, 125–140 (2017). https://doi.org/10.1016/j.scico.2017.01.002CrossRef

25.

De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program verification via iterated specialization. Sci. Comput. Progr. 95, 149–175 (2014). https://doi.org/10.1016/j.scico.2014.05.017CrossRef

26.

Peralta, J.C., Gallagher, J.P., Sağlam, H.: Analysis of imperative programs through analysis of constraint logic programs. In: Levi, G. (ed.) Static Analysis. LNCS, vol. 1503, pp. 246–261. Springer, Berlin Heidelberg (1998). https://doi.org/10.1007/3-540-49727-7_15

27.

Méndez-Lojo, M., Navas, J.A., Hermenegildo, M.V.: A flexible, (C)LP-based approach to the analysis of object-oriented programs. In: King, A. (ed.) Logic-Based Program Synthesis and Transformation. LNCS, vol. 4915, pp. 154–168. Springer, Berlin Heidelberg (2007). https://doi.org/10.1007/978-3-540-78769-3_11

28.

Gómez-Zamalloa, M., Albert, E., Puebla, G.: Decompilation of Java bytecode to Prolog by partial evaluation. Inform. Softw. Technol. 51(10), 1409–1427 (2009). https://doi.org/10.1016/j.infsof.2009.04.010CrossRef

29.

Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) Proc. 33rd ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 405–416. ACM, New York (2012). https://doi.org/10.1145/2254064.2254112

30.

De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions via program specialization. Sci. Comput. Progr. 147, 78–108 (2017). https://doi.org/10.1016/j.scico.2016.11.002CrossRef

31.

Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) Computer-Aided Verification. LNCS, vol. 9206, pp. 343–361. Springer, Berlin Heidelberg (2015). https://doi.org/10.1007/978-3-319-21690-4_20

32.

Perez-Carrasco, V., Klemen, M., López-García, P., Morales, J.F., Hermenegildo, M.V.: Cost analysis of smart contracts via parametric resource analysis. In: Pichardie, D., Sighireanu, M. (eds.) Static Analysis. LNCS, vol. 12389, pp. 7–31. Springer, Switzerland (2020). https://doi.org/10.1007/978-3-030-65474-0_2

33.

Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis and transformation. In: Proc. Int. Symp. Code Generation and Optimization, pp. 75–86. IEEE Comp. Soc., Piscataway NJ (2004). https://doi.org/10.1109/CGO.2004.1281665

34.

Apt, K.: Principles of Constraint Programming. Cambridge University Press, Cambridge UK (2003). https://doi.org/10.1017/CBO9780511615320

35.

Marriott, K., Stuckey, P.J.: Programming with Constraints: An Introduction. MIT Press, Cambridge MA (1998)

36.

Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. Logic Progr. 19(20), 503–581 (1994). https://doi.org/10.1016/0743-1066(94)90033-7MathSciNetCrossRef

37.

De Angelis, E., Fioravanti, F., Gallagher, J.P., Hermenegildo, M.V., Pettorossi, A., Proietti, M.: Analysis and transformation of constrained Horn clauses for program verification. Theory Pract. Logic Progr. 22(6), 974–1042 (2022). https://doi.org/10.1017/S1471068421000211MathSciNetCrossRef

38.

Hehner, E.: A Practical Theory of Programming. Springer, New York NY (1993)

39.

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. Fourth ACM Symp. Principles of Programming Languages, pp. 238–252. ACM, New York (1977). https://doi.org/10.1145/512950.512973

40.

Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) Programming Language Implementation and Logic Programming. LNCS, vol. 631, pp. 269–295. Springer, Berlin Heidelberg (1992). https://doi.org/10.1007/3-540-55844-6_142

41.

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Proc. Fifth ACM Symp. Principles of Programming Languages, pp. 84–96. ACM, New York (1978). https://doi.org/10.1145/512760.512770

42.

Bancilhon, F., Maier, D., Sagiv, Y., Ullman, J.D.: Magic sets and other strange ways to implement logic programs. In: Silberschatz, A. (ed.) Proc. Fifth ACM SIGMOD-SIGACT Symp. Principles of Database Systems, pp. 1–15. ACM, New York (1986). https://doi.org/10.1145/6012.15399

43.

Fioravanti, F., Pettorossi, A., Proietti, M.: Specialization with clause splitting for deriving deterministic constraint logic programs. In: Proceedings of the IEEE conference Systems, Man and Cybernetics. IEEE, Piscataway NJ (2002). https://doi.org/10.1109/ICSMC.2002.1167971

44.

Gallagher, J.P.: Tutorial on specialisation of logic programs. In: Schmidt, D. (ed.) PEPM’93: Proc. 1993 ACM SIGPLAN Symp. Partial Evaluation and Semantics-Based Program Manipulation, pp. 88–98. ACM, New York (1993). https://doi.org/10.1145/154630.154640

45.

Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) Verification, Model Checking and Abstract Interpretation. LNCS, vol. 2937, pp. 239–251. Springer, Berlin Heidelberg (2004). https://doi.org/10.1007/978-3-540-24622-0_20

46.

Sohn, K., Van Gelder, A.: Termination detection in logic programs using argument sizes. In: Rosenkrantz, D.J. (ed.) Proc. Tenth ACM SIGACT-SIGMOD-SIGART Symp. Principles of Database Systems, pp. 216–226. ACM, New York (1991). https://doi.org/10.1145/113413.113433

47.

Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library. Sci. Comput. Progr. 72(1–2), 3–21 (2008). https://doi.org/10.1016/j.scico.2007.08.001CrossRef

48.

Termination Competition 2022: C Integer. https://termcomp.github.io/Y2022/C_Integer.html. Accessed: 2023-04-26

49.

Bueno, F., Cabeza, D., Carro, M., Hermenegildo, M., López-García, P., Puebla, G.: The Ciao Prolog system: Reference manual. Technical Report CLIP 3/97.1, UPM (1997). http://www.clip.dia.fi.upm.es/

50.

Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer-Aided Verification. LNCS, vol. 8559, pp. 737–744. Springer, Berlin Heidelberg (2014). https://doi.org/10.1007/978-3-319-08867-9_49

51.

Kafle, B., Gallagher, J.P., Morales, J.F.: RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata. In: Chaudhuri, S., Farzan, A. (eds.) Computer-Aided Verification. LNCS, vol. 9779, pp. 261–268. Springer, Berlin Heidelberg (2016). https://doi.org/10.1007/978-3-319-41528-4_14

52.

Larraz, D., Nimkar, K., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving non-termination using Max-SMT. In: Biere, A., Bloem, R. (eds.) Computer-Aided Verification. LNCS, vol. 8559, pp. 779–796. Springer, Berlin Heidelberg (2014). https://doi.org/10.1007/978-3-319-08867-9_52

53.

Velroyen, H., Rümmer, P.: Non-termination checking for imperative programs. In: Beckert, B., Hähnle, R. (eds.) Tests and Proofs. LNCS, vol. 4966, pp. 154–170. Springer, Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-540-79124-9_11

54.

Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java bytecode. In: Beckert, B., Damiani, F., Gurov, D. (eds.) Formal Verification of Object-Oriented Software. LNCS, vol. 7421, pp. 123–141. Springer, Berlin Heidelberg (2012). https://doi.org/10.1007/978-3-642-31762-0_9

55.

Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.W.: Disproving termination with overapproximation. In: Claessen, K., Kuncak, V. (eds.) Formal Methods in Computer-Aided Design, pp. 67–74. FMCAD Inc, Vienna (2014). https://doi.org/10.1109/FMCAD.2014.6987597

56.

Leike, J., Heizmann, M.: Geometric nontermination arguments. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 10806, pp. 266–283. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_16

57.

Fribourg, L., Olsén, H.: A decompositional approach for computing least fixed-points of Datalog programs with \(\cal{Z} \)-counters. Constraints 2(3/4), 305–335 (1997). https://doi.org/10.1023/A:1009747629591MathSciNetCrossRef

58.

Leuschel, M., Lehmann, H.: Solving coverability problems of Petri nets by partial deduction. In: Gabbrielli, M., Pfenning, F. (eds.) Proc. Second Int. ACM SIGPLAN Conf. Principles and Practice of Declarative Programming, pp. 268–279. ACM, New York (2000). https://doi.org/10.1145/351268.351298

59.

Jaffar, J., Santosa, A.E., Voicu, R.: A CLP proof method for timed automata. In: Proc. 25th IEEE Real-Time Systems Symp., pp. 175–186. IEEE, Piscataway NJ (2004). https://doi.org/10.1109/REAL.2004.5

60.

Banda, G., Gallagher, J.P.: Analysis of linear hybrid systems in CLP. In: Hanus, M. (ed.) Logic-Based Program Synthesis and Transformation. LNCS, vol. 5438, pp. 55–70. Springer, Berlin Heidelberg (2008). https://doi.org/10.1007/978-3-642-00515-2_5

61.

Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, R. (ed.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1579, pp. 223–239. Springer, Berlin Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_16

62.

Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Proving theorems by program transformation. Fundam. Inform. 127(1–4), 115–134 (2013). https://doi.org/10.3233/FI-2013-899MathSciNetCrossRef

63.

De Angelis, E., Fioravanti, F., Meo, M.C., Pettorossi, A., Proietti, M.: Semantics and controllability of time-aware business processes. Fundam. Inform. 165(3–4), 205–244 (2019). https://doi.org/10.3233/FI-2019-1783MathSciNetCrossRef

64.

Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) Computer-Aided Verification. LNCS, vol. 8044, pp. 846–862. Springer, Berlin Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_59

65.

Hojjat, H., Rümmer, P.: The Eldarica Horn solver. In: Bjørner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1–7. IEEE, Piscataway NJ (2018). https://doi.org/10.23919/FMCAD.2018.8603013

66.

De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: A tool for verifying programs through transformations. In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 8413, pp. 568–574. Springer, Berlin Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_47

67.

Ben-Amram, A.M., Doménech, J.J., Genaim, S.: Multiphase-linear ranking functions and their relation to recurrent sets. In: Chang, B. (ed.) Static Analysis. LNCS, vol. 11822, pp. 459–480. Springer, Switzerland (2019). https://doi.org/10.1007/978-3-030-32304-2_22

68.

Fedyukovich, G., Zhang, Y., Gupta, A.: Syntax-guided termination analysis. In: Chockler, H., Weissenbacher, G. (eds.) Computer-Aided Verification, Part I. LNCS, vol. 10981, pp. 124–143. Springer, Berlin Heidelberg (2018). https://doi.org/10.1007/978-3-319-96145-3_7

69.

Le, T.C., Antonopoulos, T., Fathololumi, P., Koskinen, E., Nguyen, T.: DynamiTe: Dynamic termination and non-termination proofs. In: Proc. ACM Program. Lang. 4, OOPSLA, pp. 1–30. ACM, New York (2020). https://doi.org/10.1145/3428257

70.

Prabhu, S., Fedyukovich, G., Madhukar, K., D’Souza, D.: Specification synthesis with constrained Horn clauses. In: Proc. 42nd ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 1203–1217. ACM, New York (2021). https://doi.org/10.1145/3453483.3454104

Title: A lightweight approach to nontermination inference using Constrained Horn Clauses
Authors: Bishoksan Kafle
Graeme Gange
Peter Schachte
Harald Søndergaard
Peter J. Stuckey
Publication date: 14-03-2024
Publisher: Springer Berlin Heidelberg
Published in: Software and Systems Modeling
Print ISSN: 1619-1366
Electronic ISSN: 1619-1374
DOI: https://doi.org/10.1007/s10270-024-01161-5

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner