Relational Differential Dynamic Logic
207
References
1. Abrial, J.: Modeling in Event-B: System and Software Engineering. Cambridge
University Press (2010)
2. Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic for higher-order programs. PACMPL 1(ICFP), 21:1–21:29 (2017).
https://doi.org/10.1145/3110265
3. Azevedo de Amorim, A., Gaboardi, M., Hsu, J., Katsumata, S.: Probabilistic Relational Reasoning via Metrics. In: LICS 2019. pp. 1–19. IEEE (2019).
https://doi.org/10.1109/LICS.2019.8785715
4. Benton, N.: Simple relational correctness proofs for static analyses and program
transformations. In: Jones, N.D., Leroy, X. (eds.) POPL 2004. pp. 14–25. ACM
(2004). https://doi.org/10.1145/964001.964003
5. Bryce, D., Sun, J., Bae, K., Zuliani, P., Wang, Q., Gao, S., Schmarov, F., Kong,
S., Chen, W., Tavares, Z.: dReach homepage. http://dreal.github.io/dReach/
6. Butler, M.J., Abrial, J., Banach, R.: Modelling and Refining Hybrid Systems in
Event-B and Rodin. In: Petre, L., Sekerinski, E. (eds.) From Action Systems to Distributed Systems: The Refinement Approach, pp. 29–42. Chapman and Hall/CRC
(2016). https://doi.org/10.1201/b20053-5
7. Chicone, C.: Ordinary Differential Equations with Applications, Texts in Applied
Mathematics, vol. 34. Springer-Verlag New York, 2 edn. (2006)
8. Fainekos, G.E., Pappas, G.J.: Robustness of Temporal Logic Specifications. In:
Havelund, K., N´ u˜ nez, M., Rosu, G., Wolff, B. (eds.) Formal Approaches to Software Testing and Runtime Verification, First Combined International Workshops,
FATES 2006 and RV 2006, Revised Selected Papers. LNCS, vol. 4262, pp. 178–192.
Springer (2006). https://doi.org/10.1007/11940197 12
9. Girard, A., Pappas, G.J.: Approximate Bisimulation: A Bridge Between Computer Science and Control Theory. Eur. J. Control 17(5–6), 568–578 (2011).
https://doi.org/10.3166/ejc.17.568-578
10. Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge, MA,
USA (2000)
11. Hasuo, I., Suenaga, K.: Exercises in Nonstandard Static Analysis of Hybrid Systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp.
462–478. Springer (2012). https://doi.org/10.1007/978-3-642-31424-7 34
12. Liebrenz, T., Herber, P., Glesner, S.: Deductive Verification of Hybrid Control
Systems Modeled in Simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM
2018. LNCS, vol. 11232, pp. 89–105. Springer (2018). https://doi.org/10.1007/9783-030-02450-5 6
13. Lindel¨ of, E.: Sur l’application de la m´ ethode des approximations successives aux
´ equations diff´ erentielles ordinaires du premier ordre. Journal de math´ ematiques
pures et appliqu´ ees 4e s´ erie 10, 117–128 (1894)
14. Loos, S.M., Platzer, A.: Differential Refinement Logic. In: Grohe, M.,
Koskinen, E., Shankar, N. (eds.) LICS 2016. pp. 505–514. ACM (2016).
https://doi.org/10.1145/2933575.2934555
15. Mitsch, S., Platzer, A.: The KeYmaera X Proof IDE – Concepts on Usability in Hybrid Systems Theorem Proving. In: Dubois, C., Masci, P.,
M´ ery, D. (eds.) F-IDE@FM 2016. EPTCS, vol. 240, pp. 67–81 (2016).
https://doi.org/10.4204/EPTCS.240.5
16. Platzer, A.: KeYmaera homepage. http://symbolaris.com/info/KeYmaera.html
207
References
1. Abrial, J.: Modeling in Event-B: System and Software Engineering. Cambridge
University Press (2010)
2. Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic for higher-order programs. PACMPL 1(ICFP), 21:1–21:29 (2017).
https://doi.org/10.1145/3110265
3. Azevedo de Amorim, A., Gaboardi, M., Hsu, J., Katsumata, S.: Probabilistic Relational Reasoning via Metrics. In: LICS 2019. pp. 1–19. IEEE (2019).
https://doi.org/10.1109/LICS.2019.8785715
4. Benton, N.: Simple relational correctness proofs for static analyses and program
transformations. In: Jones, N.D., Leroy, X. (eds.) POPL 2004. pp. 14–25. ACM
(2004). https://doi.org/10.1145/964001.964003
5. Bryce, D., Sun, J., Bae, K., Zuliani, P., Wang, Q., Gao, S., Schmarov, F., Kong,
S., Chen, W., Tavares, Z.: dReach homepage. http://dreal.github.io/dReach/
6. Butler, M.J., Abrial, J., Banach, R.: Modelling and Refining Hybrid Systems in
Event-B and Rodin. In: Petre, L., Sekerinski, E. (eds.) From Action Systems to Distributed Systems: The Refinement Approach, pp. 29–42. Chapman and Hall/CRC
(2016). https://doi.org/10.1201/b20053-5
7. Chicone, C.: Ordinary Differential Equations with Applications, Texts in Applied
Mathematics, vol. 34. Springer-Verlag New York, 2 edn. (2006)
8. Fainekos, G.E., Pappas, G.J.: Robustness of Temporal Logic Specifications. In:
Havelund, K., N´ u˜ nez, M., Rosu, G., Wolff, B. (eds.) Formal Approaches to Software Testing and Runtime Verification, First Combined International Workshops,
FATES 2006 and RV 2006, Revised Selected Papers. LNCS, vol. 4262, pp. 178–192.
Springer (2006). https://doi.org/10.1007/11940197 12
9. Girard, A., Pappas, G.J.: Approximate Bisimulation: A Bridge Between Computer Science and Control Theory. Eur. J. Control 17(5–6), 568–578 (2011).
https://doi.org/10.3166/ejc.17.568-578
10. Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge, MA,
USA (2000)
11. Hasuo, I., Suenaga, K.: Exercises in Nonstandard Static Analysis of Hybrid Systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp.
462–478. Springer (2012). https://doi.org/10.1007/978-3-642-31424-7 34
12. Liebrenz, T., Herber, P., Glesner, S.: Deductive Verification of Hybrid Control
Systems Modeled in Simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM
2018. LNCS, vol. 11232, pp. 89–105. Springer (2018). https://doi.org/10.1007/9783-030-02450-5 6
13. Lindel¨ of, E.: Sur l’application de la m´ ethode des approximations successives aux
´ equations diff´ erentielles ordinaires du premier ordre. Journal de math´ ematiques
pures et appliqu´ ees 4e s´ erie 10, 117–128 (1894)
14. Loos, S.M., Platzer, A.: Differential Refinement Logic. In: Grohe, M.,
Koskinen, E., Shankar, N. (eds.) LICS 2016. pp. 505–514. ACM (2016).
https://doi.org/10.1145/2933575.2934555
15. Mitsch, S., Platzer, A.: The KeYmaera X Proof IDE – Concepts on Usability in Hybrid Systems Theorem Proving. In: Dubois, C., Masci, P.,
M´ ery, D. (eds.) F-IDE@FM 2016. EPTCS, vol. 240, pp. 67–81 (2016).
https://doi.org/10.4204/EPTCS.240.5
16. Platzer, A.: KeYmaera homepage. http://symbolaris.com/info/KeYmaera.html