Email Gateway (Aug 22 2022 at 11:02): Email Gateway (Aug 22 2022 at 11:02):From: Chantal Keller <chantal.keller@wanadoo.fr>
Post-doctoral position in interactive theorem proving
Computational Logic Center
Department of Computer Science
The University of Iowa
Applications are invited for a post-doctoral research position in the
Computational Logic Center at the University of Iowa in the area of
interactive theorem proving and verification.
The position is funded by DARPA through the HACMS program. The work will
be done in collaboration with researchers at New York University, the
Université Paris Sud and Princeton University. The main goal of the
project is to increase the level of automation in the Coq proof
assistant by soundly integrating SMT solvers into it. Our immediate
emphasis is on supporting software verification efforts by other
research groups currently funded by HAMCS. However, we expect that the
results of the integration will benefit Coq users in general.
The ideal candidate will have a Ph.D. in Computer Science, general
knowledge of formal methods, and expertise in interactive theorem
proving in higher-order logics, with substantial experience in using
Coq, Isabelle, or similar tools. Candidates should demonstrate strong
programming and formal modeling skills. Previous experience in writing
Coq tactics and plug-ins is a considerable plus. Familiarity with SMT is
welcome but not required.
The position is a full time appointment that runs initially through
August 2016 and could be renewed for another year subject to
satisfactory performance and continuous availability of funds. Review of
applications will begin immediately. The position will remain open until
filled. The start date is negotiable, but ideally it should be as soon
as possible. The starting salary is $56,000 per year, plus health and
vacation benefits.
Depending on the candidate's interests, there might be also be a
possibility to teach one course in the spring semester in the Computer
Science department as a visiting assistant professor. This is, however,
a separate position that would entail a corresponding reduction of
effort for 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 email to
cesare-tinelli@uiowa.edu with "Coq postdoc" in the subject. When sending
an application please include your CV together with a brief description
of your research accomplishments and interests, including the names of
three references.
The Computational Logic Center at the University of Iowa is jointly
headed by Professors Aaron Stump and Cesare Tinelli. In recent years, it
has consisted on average of two faculty members, 3-5 postdocs, 6-7 PhD
students and a few master's and undergraduate students. Its work has
been funded by the AFRL, AFOSR, DARPA, NASA, NSF, Intel, Rockwell
Collins, and United Technologies.
Its main areas of research are automated deduction, satisfiability
modulo theories, software verification, model checking,
verified-programming languages, and foundations of programming
languages. 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, the CVC3 and CVC4 SMT solvers, the Kind and Kind 2
model checkers, the LFSC proof framework and checker, the Darwin theorem
prover, and the StarExec solver execution service.
Last updated: Apr 26 2024 at 16:20 UTC