PhD student position in "Formal Verification via SMT Solving", Trento (Italy)

One Doctoral Student Position in Information and Communication Technologies on the research project "WORD-LEVEL FORMAL VERIFICATION VIA SMT SOLVING" is available at the International Doctorate School in Information and Communication Technologies of the University of Trento, Italy, under the joint supervision of Dr. Alessandro Cimatti, and Prof. Roberto Sebastiani.

The research activity will be carried out jointly within the Embedded Systems (ES) Research Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler (FBK), Trento, and the Software Engineering & Formal Methods (SE&FM) Research Program, at Department of Information Engineering and Computer Science (DISI) of University of Trento.

The research activity will aim at investigating and developing novel techniques, methodologies and support tools for Satisfiability Modulo Theories (SMT) for the verification of WORD-level circuit designs. This work will be part of the "Word-Level Formal Verification via SMT Solving" (WOLFLING) project. SMT tools will be developed on top of the MathSAT SMT platform, and Formal Verification tools will be developed on top of the NuSMV Model Checking platform. Both platforms are jointly developed and maintained by ES and SE&FM.

For more information, see http://disi.unitn.it/~rseba/WOLFLING-Recruit-phd.txt or contact Prof. Roberto Sebastiani at rseba at disi.unitn.it.