Postdoctoral position on Verification of Infinite-state Systems
|Professor Cesare Tinelli, Computational Logic Center|
|Department of Computer Science, The University of Iowa|
The project's overall objective is to continue the development and implementation of novel SMT-based verification/model checking techniques to verify safety properties of synchronous models of infinite-state embedded reactive software. The project investigates such topics as contract-based compositional reasoning, automatic invariant discovery, and interactive contract generation, with special focus on extending current techniques of safety analysis to the analysis of selected liveness properties. The new techniques will be implemented in the Kind 2 model checker.
The position requires a PhD in Computer Science or a closely related field with a strong background in logic and/or automated reasoning.
The ideal candidate would also have:
- Knowledge of and experience with SAT/SMT and model checking
- Experience in designing, building, or maintaining medium-sides software systems
- Excellent programming skills
- Solid programming experience in OCaml or other functional languages
- Good English writing and speaking skills
- Ability to work in a collaborative environment
- A strong commitment to research excellence
The position is a full time appointment in the Computational Logic Center at the University of Iowa, with a starting salary of $60,000/year plus benefits which include health insurance, paid leave, and access to university facilities and activities. It will start on January 14, 2019 and is expected to have a duration of up to two years, based on performance and continued availability of funds. The position will remain open until filled.
Depending on the candidate's interests, there might be an opportunity to teach one to two courses per year in the Computer Science department as a visiting instructor. This is, however, a separate position that would entail a corresponding reduction of effort in the postdoc appointment. It should be understood as an opportunity, not as a requirement for the postdoc contract.
Inquiries and applications should be sent via e-mail to to Prof. Tinelli with "Model Checking postdoc" in the subject. When sending an application please include your CV together with a brief description of your research accomplishments and interests, and the names of three references.
Computational Logic Center
The Computational Logic Center is jointly headed by Professors Omar Chowdhury, Aaron Stump, and Cesare Tinelli. In recent years, it has included on average 3-6 postdocs, 7-9 PhD students and a number of master's and undergraduate students. Its work has been funded by AFRL, AFOSR, DARPA, DOD, NASA, NSF, ONR, General Electric, Intel, Rockwell Collins, and United Technologies. Its main areas of research are automated deduction, satisfiability modulo theories, model checking, verified-programming languages, foundations of programming languages, and formal methods for security and privacy. The center has a strong emphasis on theoretical foundations but is also known for a number of languages and tools co-developed with external partners and used in academia and industry. These include the SMT-LIB standard and benchmark library, the CVC3 and CVC4 SMT solvers, the Kind and Kind 2 model checkers, the LFSC proof framework and checker, and the StarExec solver execution service.