Skip to main content
SpringerLink
Log in

Counterexample-Driven Synthesis for Probabilistic Program Sketches

  • Conference paper
  • First Online:
Book cover Formal Methods – The Next 30 Years (FM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

Included in the following conference series:

Abstract

Probabilistic programs are key to deal with uncertainty in, e.g., controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our approach leverages efficient model checking, modern SMT solving, and counterexample generation at program level. Experiments on practically relevant case studies show that design spaces with millions of candidate designs can be fully explored using a few thousand verification queries.

This work has been supported by the Czech Science Foundation grant No. GA19-24397S, the IT4Innovations excellence in science project No. LQ1602, the DFG RTG 2236 “UnRAVeL”, and the ERC Advanced Grant 787914 “FRAPPANT”,.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We focus on program-level synthesis, and refrain from discussing important implementation aspects—like how to represent \(Q\)—here.

  2. 2.

    A good implementation takes a subset of \(B' \subseteq B\) by considering the \(\texttt {Prob}(D,\lozenge B')\).

  3. 3.

    As in Sect. 3.1: A partial realisation for \(\mathfrak {S}_H\) is a function \({\bar{R} :H \rightarrow \mathsf {Option}_H \cup \{\bot \}}\) s.t. \(\forall h\in H.~\bar{R}(h) \in \mathsf {Option}_h \cup {\{ \perp \}}\). For partial realisations \(\bar{R}_1, \bar{R}_2\), let \(\bar{R}_1 \subseteq \bar{R}_2\) iff \(\forall h \in H.\;\bar{R}_1(h) \in \{ \bar{R}_2(h),\perp \}\). Let R be a realisation s.t. \(\mathfrak {S}_H(R) \not \models \varphi \) for \(\varphi \in \varPhi \). Partial realisation \(\bar{R}_{\varphi } \subseteq R\) is a conflict for \(\varphi \) iff \(\forall R' \supseteq \bar{R}_{\varphi }~\mathfrak {S}_H(R') \not \models \varphi \).

  4. 4.

    https://github.com/moves-rwth/sketching.

References

  1. Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 270–288. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_15

    Chapter  Google Scholar 

  2. Ábrahám, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.-P., Wimmer, R.: Counterexample generation for discrete-time Markov models: an introductory survey. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 65–121. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07317-0_3

    Chapter  MATH  Google Scholar 

  3. Alur, R., et al.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, vol. 40, pp. 1–25. IOS Press (2015)

    Google Scholar 

  4. Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84–93 (2018)

    Article  Google Scholar 

  5. Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bull. EATCS 95, 94–129 (2008)

    MathSciNet  MATH  Google Scholar 

  6. Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. Handbook of Model Checking, pp. 963–999. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_28

    Chapter  MATH  Google Scholar 

  7. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  8. Balsamo, S., Di Marco, A., Inverardi, P., Simeoni, M.: Model-based performance prediction in software development: a survey. IEEE Trans. Softw. Eng. 30(5), 295–310 (2004)

    Article  Google Scholar 

  9. Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326–340. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_30

    Chapter  MATH  Google Scholar 

  10. Becker, S., Koziolek, H., Reussner, R.: The Palladio component model for model-driven performance prediction. J. Syst. Softw. 82(1), 3–22 (2009)

    Article  Google Scholar 

  11. Benes, N., Kretínský, J., Larsen, K.G., Møller, M.H., Sickert, S., Srba, J.: Refinement checking on parametric modal transition systems. Acta Inf. 52(2–3), 269–297 (2015)

    Article  MathSciNet  Google Scholar 

  12. Beneš, N., Křetínský, J., Guldstrand Larsen, K., Møller, M.H., Srba, J.: Dual-priced modal transition systems with time durations. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 122–137. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28717-6_12

    Chapter  Google Scholar 

  13. Benini, L., Bogliolo, A., Paleologo, G., Micheli, G.D.: Policy optimization for dynamic power management. IEEE Trans. CAD Integr. Circ. Syst. 8(3), 299–316 (2000)

    Google Scholar 

  14. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

    Google Scholar 

  15. Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812–830 (2006)

    Article  Google Scholar 

  16. Bondy, A.B.: Foundations of Software and System Performance Engineering. Addison Wesley, Boston (2014)

    Google Scholar 

  17. Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Optimizing synthesis with metasketches. In: POPL, pp. 775–788. ACM (2016)

    Google Scholar 

  18. Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151–168. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_9

    Chapter  Google Scholar 

  19. Calinescu, R., Ghezzi, C., Johnson, K., et al.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans. Reliab. 65(1), 107–125 (2016)

    Article  Google Scholar 

  20. Calinescu, R., Ghezzi, C., Kwiatkowska, M.Z., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69–77 (2012)

    Article  Google Scholar 

  21. Calinescu, R., Češka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Designing robust software systems through parametric Markov chain synthesis. In: ICSA, pp. 131–140. IEEE (2017)

    Google Scholar 

  22. Calinescu, R., Češka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: RODES: a robust-design synthesis tool for probabilistic systems. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 304–308. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66335-7_20

    Chapter  Google Scholar 

  23. Calinescu, R., Češka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Efficient synthesis of robust models for stochastic systems. J. Syst. Softw. 143, 140–158 (2018)

    Article  Google Scholar 

  24. Cardelli, L., et al.: Syntax-guided optimal synthesis for chemical reaction networks. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 375–395. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_20

    Chapter  Google Scholar 

  25. Černý, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243–259. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_20

    Chapter  Google Scholar 

  26. Češka, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. Acta Inf. 54(6), 589–623 (2017)

    Article  MathSciNet  Google Scholar 

  27. Češka, M., Jansen, N., Junges, S., Katoen, J.-P.: Shepherding hordes of Markov chains. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 172–190. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_10

    Chapter  Google Scholar 

  28. Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for markov decision processes. ACM Trans. Comput. Log. 12(1), 1:1–1:49 (2010)

    Article  MathSciNet  Google Scholar 

  29. Chatterjee, K., Chmelik, M., Davies, J.: A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. In: AAAI, pp. 3225–3232. AAAI Press (2016)

    Google Scholar 

  30. Chaudhuri, S., Clochard, M., Solar-Lezama, A.: Bridging boolean and quantitative synthesis using smoothed proof search. In: POPL. ACM (2014)

    Google Scholar 

  31. Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE, pp. 85–92. IEEE (2013)

    Google Scholar 

  32. Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput. 30(1), 45–75 (2018)

    Article  MathSciNet  Google Scholar 

  33. Dehnert, C., Jansen, N., Wimmer, R., Ábrahám, E., Katoen, J.-P.: Fast debugging of PRISM models. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 146–162. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11936-6_11

    Chapter  Google Scholar 

  34. Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_31

    Chapter  Google Scholar 

  35. Delahaye, B., et al.: Abstract probabilistic automata. Inf. Comput. 232, 66–116 (2013)

    Article  MathSciNet  Google Scholar 

  36. Dureja, R., Rozier, K.Y.: More scalable LTL model checking via discovering design-space dependencies (\(D^{3}\)). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 309–327. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_17

    Chapter  Google Scholar 

  37. Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Softw. Eng. 42(1), 75–99 (2016)

    Article  Google Scholar 

  38. Fiondella, L., Puliafito, A. (eds.): Principles of Performance and Reliability Modeling and Evaluation. SSRE. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30599-8

    Book  Google Scholar 

  39. Gerasimou, S., Tamburrelli, G., Calinescu, R.: Search-based synthesis of probabilistic models for quality-of-service software engineering. In: ASE, pp. 319–330. IEEE Computer Society (2015)

    Google Scholar 

  40. Ghezzi, C., Sharifloo, A.M.: Model-based verification of quantitative non-functional properties for software product lines. Inf. Softw. Technol. 55(3), 508–524 (2013)

    Article  Google Scholar 

  41. Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends Programm. Lang. 4(1–2), 1–119 (2017)

    Google Scholar 

  42. Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. Softw. Tools Technol. Transf. 13(1), 3–19 (2011)

    Article  Google Scholar 

  43. Henzinger, T.A.: Quantitative reactive modeling and verification. Comput. Sci.- Res. Dev. 28(4), 331–344 (2013)

    Article  Google Scholar 

  44. Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_3

    Chapter  Google Scholar 

  45. Jansen, N., Humphrey, L.R., Tumova, J., Topcu, U.: Structured synthesis for probabilistic systems. CoRR abs/1807.06106, at NFM 2019 (2018, to appear)

    Google Scholar 

  46. Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.-P.: Safety-constrained reinforcement learning for MDPs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 130–146. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_8

    Chapter  Google Scholar 

  47. Junges, S., et al.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI, pp. 519–529. AUAI Press (2018)

    Google Scholar 

  48. Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101(1–2), 99–134 (1998)

    Article  MathSciNet  Google Scholar 

  49. Křetínský, J.: 30 years of modal transition systems: survey of extensions and analysis. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 36–74. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_3

    Chapter  MATH  Google Scholar 

  50. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  51. Kwiatkowska, M.Z., Norman, G., Parker, D., Vigliotti, M.G.: Probabilistic mobile ambients. Theor. Comput. Sci. 410(12–13), 1272–1303 (2009)

    Article  MathSciNet  Google Scholar 

  52. Larsen, K.G.: Verification and performance analysis of embedded and cyber-physical systems using UPPAAL. In: MODELSWARD 2014, pp. IS-11 (2014)

    Google Scholar 

  53. Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE Computer Society (1988)

    Google Scholar 

  54. Lindemann, C.: Performance modelling with deterministic and stochastic Petri nets. Perf. Eval. Review 26(2), 3 (1998)

    Article  MathSciNet  Google Scholar 

  55. Meuleau, N., Kim, K.E., Kaelbling, L.P., Cassandra, A.R.: Solving POMDPs by searching the space of finite policies. In: UAI, pp. 417–426. Morgan Kaufmann Publishers Inc. (1999)

    Google Scholar 

  56. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  57. Nori, A.V., Ozair, S., Rajamani, S.K., Vijaykeerthy, D.: Efficient synthesis of probabilistic programs. In: PLDI, pp. 208–217. ACM (2015)

    Google Scholar 

  58. Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50–67. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_4

    Chapter  MATH  Google Scholar 

  59. Rodrigues, et al.: Modeling and verification for probabilistic properties in software product lines. In: HASE, pp. 173–180. IEEE (2015)

    Google Scholar 

  60. Rosenblum, D.S.: The power of probabilistic thinking. In: ASE, p. 3. ACM (2016)

    Google Scholar 

  61. Sharma, V.S., Trivedi, K.S.: Quantifying software performance, reliability and security: an architecture-based approach. J. Syst. Softw. 80(4), 493–509 (2007)

    Article  Google Scholar 

  62. Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: PLDI, pp. 136–148. ACM (2008)

    Google Scholar 

  63. Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI, pp. 281–294. ACM (2005)

    Google Scholar 

  64. Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404–415. ACM (2006)

    Google Scholar 

  65. Stewart, W.J.: Probability, Markov Chains, Queues, and Simulation: The Mathematical Basis of Performance Modeling. Princeton university press (2009)

    Google Scholar 

  66. Vandin, A., ter Beek, M.H., Legay, A., Lluch Lafuente, A.: QFLan: a tool for the quantitative analysis of highly reconfigurable systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 329–337. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-95582-7_19

    Chapter  Google Scholar 

  67. Varshosaz, M., Khosravi, R.: Discrete time Markov chain families: modeling and verification of probabilistic software product lines. In: SPLC Workshops, pp. 34–41. ACM (2013)

    Google Scholar 

  68. Češka, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-driven synthesis for probabilistic program sketches. CoRR abs/1904.12371 (2019)

    Google Scholar 

  69. Vlassis, N., Littman, M.L., Barber, D.: On the computational complexity of stochastic controller optimization in POMDPs. ACM Trans. Comput. Theor. 4(4), 12:1–12:8 (2012). https://doi.org/10.1145/2382559.2382563

    Article  MATH  Google Scholar 

  70. Wimmer, R., Jansen, N., Ábrahám, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time Markov models. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299–314. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_21

    Chapter  MATH  Google Scholar 

  71. Wimmer, R., Jansen, N., Vorpahl, A., Ábrahám, E., Katoen, J.-P., Becker, B.: High-Level Counterexamples for Probabilistic Automata. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 39–54. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_4

    Chapter  Google Scholar 

  72. Woodside, M., Petriu, D., Merseguer, J., Petriu, D., Alhaj, M.: Transformation challenges: from software models to performance models. J. Softw. Syst. Model. 13(4), 1529–1552 (2014)

    Article  Google Scholar 

  73. Wu, S., Smolka, S.A., Stark, E.W.: Composition and behaviors of probabilistic I/O automata. Theor. Comput. Sci. 176(1–2), 1–38 (1997)

    Article  MathSciNet  Google Scholar 

  74. Zhou, W., Li, W.: Safety-aware apprenticeship learning. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 662–680. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_38

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Brno University of Technology, FIT, IT4I Centre of Excellence, Brno, Czech Republic

    Milan Češka

  2. RWTH Aachen University, Aachen, Germany

    Christian Hensel, Sebastian Junges & Joost-Pieter Katoen

Authors
  1. Milan Češka
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Hensel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sebastian Junges
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Joost-Pieter Katoen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sebastian Junges .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Češka, M., Hensel, C., Junges, S., Katoen, JP. (2019). Counterexample-Driven Synthesis for Probabilistic Program Sketches. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation