15-424: Foundations of Cyber-Physical Systems (Sp'17)

Table of Contents
  1. KeYmaera X Usage
  2. Old: KeYmaera 3 Usage
  3. Typesetting Proofs
  4. Further Reading
    1. Ordinary Differential Equations
    2. First-Order Logic

KeYmaera X Usage

Old: KeYmaera 3 Usage

Previous instances of this course were using KeYmaera, the precursor of the more advanced theorem prover KeYmaera X. Your mileage from the KeYmaera documentation may vary, because it is thorough, but not adapted to KeYmaera X.
Starring KeYmaera on YouTube Channel KeYmaera Documentation

Typesetting Proofs

You are encouraged to typeset your theory homework solutions. Scans of handwritten homework solutions of a similarly high quality will be accepted. But if we cannot decipher your homework, we cannot give you any points for it.

Different packages exist for typesetting proofs in LaTeX. They have different advantages and downsides so it may be a matter of personal preference which one works best for you.

Further Reading

This course will make heavy use of differential equations, logic and theorem proving. While each of those topics will be discussed in this course, you are expected to be able to get up to speed quickly. Depending on your prior background and how well you remember this material from other courses, we recommend that you look at some of the following resources before the semester starts. This will make it easier for you to get going in cyber-physical systems. You may also find these resources helpful for extra reading throughout the semester.

You should feel very comfortable with the elementary background material, e.g., what a differential equation is, before the course begins. We also include advanced materials for interested students.

We will also add further reading material as the course progresses.

  1. André Platzer.
    Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 pages. ISBN 978-3-642-14508-7.
    [bib | doi | book | web]

  1. [e-book in CMU Library]

Ordinary Differential Equations

First-Order Logic