[SMT-LIB] Postdoc position at the University of Iowa

[Cesare Tinelli]

Postdoc position in Verification of Infinite-state Systems
(Updated Nov 2, 2016)
http://www.cs.uiowa.edu/~tinelli/html/positions.html


Project Supervisor

Professor Cesare Tinelli, Computational Logic Center
Department of Computer Science, The University of Iowa
http://www.cs.uiowa.edu/~tinelli


Project Description

The project's overall objective is to develop and implement improved 
SMT-based
verification/model checking techniques to verify safety properties of 
synchronous
data-flow models of infinite-state embedded reactive software. The 
project will
focus on contract-based compositional reasoning, automatic invariant 
discovery,
static analysis of contracts, and interactive contract generation. The 
new
techniques will be implemented in the Kind 2 model checker.


Position

The ideal candidate would be one with:
- A PhD in Computer Science or a closely related field
- A strong background in logic and/or automated reasoning
- Knowledge of and experience with SAT/SMT and model checking
- Experience designing, building, and maintaining large software systems
- Excellent programming skills
- Solid programming experience in OCaml or similar languages
- Good English writing and speaking skills
- The 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, with a
starting salary of $58,000/year plus benefits which include health 
insurance, paid
leave, and access to university facilities and activities.
It will start on **January 1, 2017** 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
course per year in the Computer Science department as a visiting 
assistant professor.
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-5
postdocs, 6-8 PhD students and a number of master's and undergraduate 
students.
Its work has been funded by AFRL, AFOSR, DARPA, DOD, NASA, NSF, 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.