Postdoc position at Carnegie Mellon University on Hybrid Systems Theorem Proving
Postdoc position: Hybrid Systems Theorem Proving Carnegie Mellon University, Computer Science Department
Professor Andre Platzer is looking for talented researchers with a strong research track record for a project in the Computer Science Department of Carnegie Mellon University. The aim of the research is to develop next-generation verification techniques for cyber-physical systems and hybrid systems.
Our research group develops logical foundations for cyber-physical systems (CPS), i.e., systems that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPS applications abound. Ensuring their correct functioning, however, is a serious challenge. Scientists and engineers need analytic tools to understand and predict the behavior of their systems. That's the key to designing smart and reliable control. These foundations have been implemented in our theorem prover KeYmaera and have found application in the verification of cars, aircraft, railway systems, surgical robots, and mobile robots as well as in a number of courses. This research project will develop the next-generation KeYmaera to advance the state of the art in cyber-physical systems verification and enable efficient verification of complex application scenarios.
Strong applicants will have a background in formal verification and strong functional programming skills. Candidates should have a PhD (or equivalent) in Computer Science or a closely related subject. Suitable applicants nearing completion of a PhD will be considered. The successful candidate will have the opportunity to collaborate with the students and faculty in the Logical Systems Lab on different aspects of our research agenda. Relevant research topics include sequent calculus, automated theorem proving, invariant generation, proof tactics, and differential invariants.
Interested candidates should send their CV, research statement, and list of references to Professor Andre Platzer at aplatzer@cs.cmu.edu