Start date: 2010 Expected completion date: 2013
PIs : João Paulo Marques Silva (INESC ID / IST/UTL) and Edmund M. Clarke (CMU)
Teams: INESC ID, Instituto Superior Técnico / Universidade Técnica de Lisboa (IST/UTL), Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa (FCT/UNL), Carnegie Mellon University (CMU)
Company: Caixa Mágica Software
Keywords: Software Verification; Model Checking; Decision Procedures; Proof Certificates
The project is organized into three main themes related to the development of tools for verification of certified software. The first theme involves carrying out research work on the topic of decision-making procedures for verification of software, including the development of decision procedures capable of producing certificates to validate the correctness of the results. The second theme is the development of procedures for deciding certificates, or procedures that produce results guaranteed correct. The third theme is the development of a model checker for supported decision-making procedures certificates, thus proving the correctness of the results. The decision procedures studied in the project will include techniques of Boolean constraint satisfaction, finite domain and continuous domain in which they have verified the modeling software, which is also expected that applicants have a doctorate in the field of Constraint Programming (CP ) and / or Boolean Constraint Satisfaction (SAT).
Examples of protypes are the following:
1. RAReQS, a QBF solver using abstraction refinement: http://sat.inesc-id.pt/~mikolas/sw/areqs/
2. GhostQ, a QBF solver that can produce certificates of correctness: http://www.cs.cmu.edu/~wklieber/ghostq/
Presentation about the ATTEST project pdf (“ICT Portugal Workshop: New Projects in Networks, Software, Energy and Security”, March 2011)
Articles published in the Portuguese media:
Joining Universities and Industries Can Create Value to Portugal (Ciência Hoje, March 2011)
