CSD Home | Research Home

 

 

Acar
Andersen
Blelloch
Blum, A.
Blum, L.
Blum, M.
Brookes
Brunskill
Bryant
Carbonell
Christel
Clarke
Crary
Dannenberg
Datta
Erdmann
Fahlman
Faloutsos
Fatahalian
Fink
Garlan
Gibson
Goldstein
Gupta
Guruswami
Harchol-Balter
Harper
Hauptmann
Hodgins

Kanade
Kolter
Lee, T.

Mason
Maxion

Miller
Mitchell
Morris
Mowry
O'Donnell
O'Hallaron
Pavlo
Pfenning
Platzer
Pollard
Procaccia
Reddy
Rudich
Rudnicky
Sandholm
Satyanarayanan
Schmerl
Seshan
Shaw
Siewiorek
Simmons
Sleator
Steenkiste
Touretzky
Treuille
Veloso
Von Ahn
Wactlar
Wing
Zhang
 
Affiliated Faculty
Aldrich
Brumley
Durand
Ganger
Hoe
Mutlu
Perrig
Schwartz
Stern
Xing
Yang

Andre Platzer
Assistant Professor, Computer Science
www

I work in the areas of logic in computer science, cyber-physical systems, programming languages, and formal methods. Below are short descriptions of some of my research topics and directions.

Logic of Dynamical Systems

Logic of dynamical systems studies logics and proof principles for properties of dynamical systems. Dynamical systems are mathematical models describing how the state of a system evolves over time. They are important in modeling and understanding many applications, including embedded systems and cyber-physical systems (CPSs). CPSs combine cyber capabilities (computation and/or communication) with physical capabilities (motion or other physical processes) to solve problems that no part could solve alone. Cars, aircraft and robots are prime examples, because they move physically in space in a way that is determined by discrete computerized control algorithms. Designing these algorithms to control CPSs is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safety-critical tasks like keeping aircraft from colliding.

"How can we provide people with cyber-physical systems they can bet their lives on?" [Jeannette Wing]

I develop the logical foundations of cyber-physical systems. I study the theory, practice, and applications of logics of dynamical systems and their use in verification. This relatively young area is a promising direction for future research, unique in its manifold connections to other pure and applied sciences, including many areas of mathematics, physics, and control theory.

KeYmaera: A Hybrid Theorem Prover for Hybrid Systems

KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic (dL), which is a first-order dynamic logic for hybrid programs, a program notation for hybrid systems. KeYmaera supports hybrid systems with nonlinear discrete jumps, nonlinear differential equations, differential-algebraic equations, differential inequalities, and systems with nondeterministic discrete or continuous input. For automation, KeYmaera implements a free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. This compositional verification principle helps scaling up verification, because KeYmaera verifies a big system by verifying properties of subsystems. To overcome the complexity of real arithmetic, we integrate real quantifier elimination and other decision procedures following an iterative background closure strategy. The KeYmaera verification tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying case studies from train control, car control, air traffic control, and robotics.

      CSD Home   Webteam  ^ Top   SCS Home