Logic List Mailing Archive

Postdoctoral position in hybrid systems theorem proving, Pittsburgh PA (U.S.A.)

Postdoc position: Hybrid Systems Theorem Proving
Carnegie Mellon University, Computer Science Department

Professor Andr 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


Andre Platzer
http://www.cs.cmu.edu/~aplatzer/