The research problem addressed by this project is the development of techniques and tools for the automated discovering of loop invariants. Infinite program fragments such as loops or recursive functions should be represented by a finite summary, i.e., an invariant, in order to succeed in their verification. Moreover, retrieving an invariant it’s mandatory if we want to model check function handling unbounded data structures (e.g., a function that sorts an input array of unknown length). Such invariants are represented as quantified formula over the variables of the program.
As an overall goal, this project proposes new invariant discovery methods which will enhance and make more productive already developed security-oriented frameworks. The problem of synthesizing invariants is linked to the problem of finding suitable abstraction algorithms for extracting relevant system information that will be used to derive invariants as first-order formula.
Three requirements are mandatory in order to synthesize useful invariants for the aforementioned systems: (i) we need to be able to model check infinite-state systems, as parameterization, loops and recursion are sources of infiniteness (ii) we need to handle natively and efficiently quantifiers, as suitable predicates about systems handling unbounded data structures are quantified literals and (iii) a suitable abstraction technique must be defined in order to be able to synthesize suitable invariants, for solving effectively and efficiently safety checks.
This project is supported by the Hasler Foundation.
