WP2 - Reasoning Tasks for Specification and Verification
Partners Involved: SAU / INRIA / UNC / UBA
The main goal of this work package is to investigate theoretical (e.g., model theory, complexity, expressiveness) and practical (e.g., implementation, heuristics, testing) issues of logical frameworks used for specification and verification. We have identified three main research challenges that the work package will address:
- Simulation. We will investigate notions of simulation for different languages, and define a framework in which general results (e.g., the van Benthem Characterization Theorem) can be uniformly obtained. We will pay special attention to languages without negation and languages with binding operators. Lack of negation makes the notion of simulation not necessarily symmetric, introducing additional complexity. Similarly, binding operators introduce dependencies between different operators which, again, complicate analysis.
- Automated and semi-automated tools for the verification of distributed algorithms. We will advance the state of the art of combining interactive and automated deduction methods and tools, with the objective of (semi)automatically verifying distributed systems and protocols. Special attention will be devoted to the design of appropriate decision procedures, their integration into SMT solvers and first-order theorem provers, and certification of results within logical frameworks. These techniques will be applied to distributed algorithms, ensuring that they scale to problems that are relevant in practical applications.
- Verification of systems with data. A serious limitation for most model- checking techniques to verify infinite-state systems rests on the fact that they are mainly interested on the control and less on the data values stored by local or global program variables. Our goal is to develop and refine specification languages for properties on data that can lead to verification techniques for systems heavily manipulating data. We will resort to abstract interpretation techniques to further advance here. Reasoning with data in specific structures has been considered for arrays, for memory states or for XML documents to quote a few examples.
