208
J. Kolˇ c´ ak et al.
17. Platzer, A.: KeYmaera X homepage. http://www.ls.cs.cmu.edu/KeYmaeraX/
index.html
18. Platzer, A.: Differential Dynamic Logic for Hybrid Systems. J. Autom. Reasoning
41(2), 143–189 (2008). https://doi.org/10.1007/s10817-008-9103-8
19. Platzer, A.: The Complete Proof Theory of Hybrid Systems. In: LICS 2012. pp.
541–550. IEEE Computer Society (2012). https://doi.org/10.1109/LICS.2012.64
20. Platzer, A.: A Complete Uniform Substitution Calculus for Differential Dynamic Logic. J. Autom. Reasoning 59(2), 219–265 (2017).
https://doi.org/10.1007/s10817-016-9385-1
21. Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer (2018).
https://doi.org/10.1007/978-3-319-63588-0
22. Platzer, A., Tan, Y.K.: Differential Equation Axiomatization: The Impressive
Power of Differential Ghosts. In: Dawar, A., Gr¨ adel, E. (eds.) LICS 2018. pp.
819–828. ACM (2018). https://doi.org/10.1145/3209108.3209147
23. Robinson, A.: Non-standard analysis. Princeton University Press (1966)
24. Suenaga, K., Hasuo, I.: Programming with Infinitesimals: A While-Language for
Hybrid System Modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011.
LNCS, vol. 6756, pp. 392–403. Springer (2011). https://doi.org/10.1007/978-3-64222012-8 31
25. Suenaga, K., Sekine, H., Hasuo, I.: Hyperstream processing systems: nonstandard
modeling of continuous-time signals. In: Giacobazzi, R., Cousot, R. (eds.) POPL
2013. pp. 417–430. ACM (2013). https://doi.org/10.1145/2429069.2429120
26. Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs. In: Lahiri, S.K.,
Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 476–493. Springer (2018).
https://doi.org/10.1007/978-3-030-01090-4 28
27. Wolfram Research, Inc.: Mathematica, Version 12.0 (2019), https://www.wolfram.
com/mathematica, Champaign, IL
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.
J. Kolˇ c´ ak et al.
17. Platzer, A.: KeYmaera X homepage. http://www.ls.cs.cmu.edu/KeYmaeraX/
index.html
18. Platzer, A.: Differential Dynamic Logic for Hybrid Systems. J. Autom. Reasoning
41(2), 143–189 (2008). https://doi.org/10.1007/s10817-008-9103-8
19. Platzer, A.: The Complete Proof Theory of Hybrid Systems. In: LICS 2012. pp.
541–550. IEEE Computer Society (2012). https://doi.org/10.1109/LICS.2012.64
20. Platzer, A.: A Complete Uniform Substitution Calculus for Differential Dynamic Logic. J. Autom. Reasoning 59(2), 219–265 (2017).
https://doi.org/10.1007/s10817-016-9385-1
21. Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer (2018).
https://doi.org/10.1007/978-3-319-63588-0
22. Platzer, A., Tan, Y.K.: Differential Equation Axiomatization: The Impressive
Power of Differential Ghosts. In: Dawar, A., Gr¨ adel, E. (eds.) LICS 2018. pp.
819–828. ACM (2018). https://doi.org/10.1145/3209108.3209147
23. Robinson, A.: Non-standard analysis. Princeton University Press (1966)
24. Suenaga, K., Hasuo, I.: Programming with Infinitesimals: A While-Language for
Hybrid System Modeling. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011.
LNCS, vol. 6756, pp. 392–403. Springer (2011). https://doi.org/10.1007/978-3-64222012-8 31
25. Suenaga, K., Sekine, H., Hasuo, I.: Hyperstream processing systems: nonstandard
modeling of continuous-time signals. In: Giacobazzi, R., Cousot, R. (eds.) POPL
2013. pp. 417–430. ACM (2013). https://doi.org/10.1145/2429069.2429120
26. Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs. In: Lahiri, S.K.,
Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 476–493. Springer (2018).
https://doi.org/10.1007/978-3-030-01090-4 28
27. Wolfram Research, Inc.: Mathematica, Version 12.0 (2019), https://www.wolfram.
com/mathematica, Champaign, IL
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.