References

LS-Lab · Jan 4, 2021 · 2036d36 · 2036d36
1 parent 60ca169
commit 2036d36
Show file tree

Hide file tree

Showing 7 changed files with 27 additions and 3 deletions.
diff --git a/examples/README.md b/examples/README.md
@@ -1,5 +1,5 @@
 # Examples
-Examples, models, and proofs in KeYmaera X, which is an aXiomatic Tactical Theorem Prover KeYmaera X for Hybrid Systems.
+Interesting simple but instructive examples, models, and proofs in KeYmaera X, which is an aXiomatic Tactical Theorem Prover KeYmaera X for Hybrid Systems.
 
   http://keymaeraX.org/
 

diff --git a/games/README.md b/games/README.md
@@ -5,3 +5,8 @@ Provides a number of instructive simple examples for how to prove hybrid games.
 
   http://keymaeraX.org/
 
+# References
+
+André Platzer. 
+[Logical Foundations of Cyber-Physical Systems](https://doi.org/10.1007/978-3-319-63588-0). 
+Springer, Cham, 2018.
diff --git a/ijrr/README.md b/ijrr/README.md
@@ -11,6 +11,8 @@ can be guaranteed despite sensor uncertainty and actuator perturbation. We compl
 safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot
 navigate waypoints and pass intersections.
 
+# References
+
 Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, André Platzer.
 [Formal verification of obstacle avoidance and navigation of ground robots](https://doi.org/10.1177/0278364917733549).
 International Journal of Robotics Research. 36(12), pp. 1312-1340, 2017. 

diff --git a/lfcps-tutorial/README.md b/lfcps-tutorial/README.md
@@ -5,4 +5,10 @@ Provides a number of instructive simple examples from the lectures on Logical Fo
 [Marktoberdorf Summer School on Safety and Security of Software Systems: Logics, Proofs, Applications, Marktoberdorf, Germany, 08/2019.](https://asimod.in.tum.de/).
 
   http://keymaeraX.org/
+  MOD'19 Tutorial
 
+# References
+
+André Platzer. 
+[Overview of logical foundations of cyber-physical systems](https://arxiv.org/abs/1910.11232). 
+In Helmut Seidl and Mooly Sagiv, editors, Marktoberdorf 2019, Summer School on Safety and Security of Software Systems: Logics, Proofs, Applications, Marktoberdorf, Germany, July 31 to August 9, 2019.
diff --git a/lfcps/README.md b/lfcps/README.md
@@ -1,11 +1,15 @@
 Logical Foundations of Cyber-Physical Systems Textbook Examples
 ===============================================================
 
-Provides examples from the 2018 textbook
+Provides examples from the 2018 textbook on Logical Foundations of Cyber-Physical Systems.
+
+  http://keymaeraX.org/
+  LFCPS Tutorial
+
+# References
 
 André Platzer. 
 [Logical Foundations of Cyber-Physical Systems](https://lfcps.org/lfcps/). 
 [Springer](https://doi.org/10.1007/978-3-319-63588-0), Cham, 2018. 
 
-  http://keymaeraX.org/
 
diff --git a/popltutorial/README.md b/popltutorial/README.md
@@ -6,3 +6,8 @@ Provides a number of instructive simple examples from the
 
   http://keymaeraX.org/
 
+# References
+
+André Platzer.
+[Programming Cyber-Physical Systems With Logic](https://popl19.sigplan.org/event/popl-2019-tutorialfest-t4-programming-cyber-physical-systems-with-logic).
+POPL 2019 Tutorials.
diff --git a/roundabout/README.md b/roundabout/README.md
@@ -9,5 +9,7 @@ of aircraft throughout their flight. We show that formal verification of hybrid
 required in aircraft control applications. We introduce a fully flyable variant of the roundabout collision avoidance maneuver 
 and verify safety properties by compositional verification.
 
+# References
+
 André Platzer and Edmund M. Clarke. [Formal verification of curved flight collision avoidance maneuvers: A case study.](https://doi.org/10.1007/978-3-642-05089-3_35)
 In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pp. 547-562. Springer, 2009.