Project Ideas - LS-Lab/KeYmaeraX-release GitHub Wiki

Share ideas for KeYmaera X projects here. This is geared toward the course 15-424 at CMU, but some of the projects may be appropriate for general research projects as well.

Note for 15-424 students:

In our experience, students who come up with their own projects ideas have generally done better than students who took the suggested projects. I think this is because they are generally more excited about their own project ideas. So please do think of some projects of your own as well! This is meant to be a please to help people collectively come up with good ideas, as opposed to telling everyone what they ought to be doing.

Advice for course projects: Picking an exciting topic for your course project will already make it a lot of fun, but in addition to making your project fun you also need to keep an eye on the technical side of things. A top-quality final project will take advantage of a variety of different proving techniques we learn throughout the semester (i.e. it will use techniques that only come up in Labs 3 and 4), but will be structured to start with easy models and progress to hard models. As you think about project ideas, think about how the different techniques you're learning could be used.

Note the categories below are not mutually exclusive. For example if you implement some interesting theorem-proving feature, then the theory will justify why you implemented the right thing. Or if you pick a small theory problem and want a stretch goal, then you could do some implementation to help evaluate the theory.

Modeling + Proving Projects:

• Action movie stunts: e.g. The Man with the Golden Gun Barrel Roll (Fun fact: this stunt was planned with the help of physics simulations - in 1974!), Mission Impossible Vault Scene, The Spy Who Loved Me Ski Jump, Goldeneye Dam Jump
• Extreme sports: Skateboarding, Surfing, Skydiving, Stock Car Racing, etc.
• Chemistry, Biology
• More traditional CPS domains: Robotics, Space, Planes, Trains, Automobiles, Power Plants.
• A thermostat which controls one or more rooms.
• Proportional-integral-derivative (PID) controllers.
• Insulin pumps, pace makers, or other medical devices.
• Electrical circuits.
• Chemical reactions.
• Biological systems, for example predator/prey systems.
• Use dL to solve the duck and fox interview question.
• The Knight Rider signature move.
• Extend the later labs in significant ways, e.g. by adding noisy sensors, extra obstacles, better distance measures, etc.
• Improvements to the integrator (existing source code)

Theory Projects:

• dL is just one of many so-called dynamic logics, all of which use a box modality [a] to reason about different kinds of programs. Explore other varieties of dynamic logic, or design a new dynamic logic to model your favorite kind of program or even program-like models of things that aren't programs (e.g. biological models)
• Explore the relationship between dL and other models of CPS, such as hybrid automata. And/or compare its computational and/or proof-theoretic strength with various kinds of automata.
• The KeYmaera X proof language is actively developed and has a mathematically rigorous formal definition. Extend the theory for the KeYmaera X proof language with a new feature (e.g. function definitions, easier ways to refer to formulas (no more hideL(-386592365936)) or simplify arithmetic). Or add a new feature to dL itself that makes it easier to write down your favorite models, or come up with a brand new proof language.

Implementation Projects:

• KeYmaera X Grade Maximizer: Implement a feature in KeYmaera X that checks for commonly recurring modeling mistakes.
• Get the course labs running on a real robot.
• Identify an interesting class of ODEs and/or properties of ODEs and implement tactics to prove them.
• Improve KeYmaera X UI to make it easier to understand what goes wrong in a proof. Or come up with an entirely new style of UI.