Description: André Platzer is the Alexander von Humboldt Professor at Karlsruhe Institute of Technology. He develops logics for dynamical systems to characterize the logical foundations of cyber-physical systems and to answer the question how we can trust a computer to control physical processes.
programming languages (130) formal methods (49) cyber-physical systems (16) theorem proving (7) logic in computer science (3) andré platzer (2) alexander von humboldt professor (2) logic of dynamical systems (2) logic of autonomous dynamical systems (2) karlsruhe institute of technology carnegie mellon university
André Platzer is the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology and leads the Logical Systems Lab at Carnegie Mellon University . He develops logics for dynamical systems to characterize the logical foundations of cyber-physical systems and to answer the question how we can trust a computer to control physical processes. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. Prof. Platzer pu
[ AvH Video (2min) | Brief Video (10min) | Overview Video (40min) | More Videos ]
The KeYmaera X aXiomatic Theorem Prover for Hybrid Systems is a verification tool. It is based on differential dynamic logic , which provides the Logical Foundations of Cyber-Physical Systems as explained in a recent textbook .
KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems
André Platzer @ Karlsruhe Institute of Technology
Yong Kiam Tan
KeYmaera Software: A Hybrid Theorem Prover for Hybrid Systems
KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems
Samuel Teuber