[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.
