[TYPES/announce] Postdoc position in Verification of Infinite-state Systems

[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 at the
University of Iowa, 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 at the University of Iowa 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20161102/1e43838c/attachment.html>