Andre Platzer
Location: (Pittsburgh, PA)
Personal Research Web Page: http://symbolaris.com/
Keywords: Logic, Hybrid systems, Formal methods, Formal Verification, Cyber-physical systems, Embedded systems, Automated theorem proving, Model checking, Mobile Ubiquitous Embedded Computing, Programming Languages, Compilers Software Engineering
Posted on: Friday, May 6th, 2011
Broad Research Area: AI / Machine Learning / Robotics / Vision, Mobile / Ubiquitous / Embedded Computing, Numerical/Scientific Computing / HPC / Data-Intensive Scalable Computing, Other, Programming Languages / Compilers, Theory / Algorithms
Research Interests:
My group focuses on verification of embedded and cyber-physical systems, studying the question “how can we build computerized controllers for physical systems that are guaranteed to meet their design goals?” These questions are of crucial importance in many areas, including automotive, aeronautics, railway, mobile robotics, factory automation, and medical devices. After all, our society cannot afford to have these systems malfunction. In our research, we have developed powerful logic-based verification techniques that help producing reliable complex systems, e.g., in aeronautical, railway, and automotive applications. We have developed KeYmaera, the first theorem prover for hybrid systems. We also developed the first verification technique for distributed hybrid systems, which combine the challenges of hybrid systems with those of distributed systems. We have further developed the first logic and compositional verification technique for stochastic hybrid systems. My grou p also works on statistical model checking techniques. There are plenty of exciting challenges ahead in these and related directions of research.
Contact Information:
email obfuscated - click to reveal.edu
http://symbolaris.com/
