The AMIS project is a theoretical research project coordinated by Arnaud Carayol. It also involves Christopher Broadbent, Axel Haddad, Matthew Hague, Antoine Meyer, Chloé Rispal et Oliver Serre. The project started in January 2011 for a duration of 36 months. It was funded entirely by an ANR grant of 103,160 €. <br />
The world’s complexity forbids us to accurately predict its behaviour. Scientists therefore have to come up with models and sufficiently faithful abstractions in order to try and understand it. Regarding computer science, it is sometimes very important to be able to guarantee that a given program or system meets its specifications, and if possible through an automatic process. Models for computer programs, such as Turing machines and Church’s ?-calculus, were created at the early stages of our discipline, but their automatic verification is made impossible by the undecidability problem. It is therefore necessary to consider simpler computation models, whose automatic verification is possible but which still retain enough expressiveness to be able to illustrate interesting behaviours of real programs. This project’s main contribution was to implement a verification tool for so-called functional programs, whose main feature is that functions are allowed to manipulate other functions, either as parameters or as return values. Many programming languages such as CaML, Python, C++, C# or Java, were either designed specifically for, or enriched with, functional features.
The above-mentioned undecidability result does not directly enable us to verify any functional program as a whole. It is necessary to transform it first into an abstract model which ignores some of its aspects. Higher order recursive schemes (or simply program schemes) provide a faithful abstraction of functional programs. Results due to Ong in 2006 show that many properties of these models can be automatically verified. Two tasks thus arise: to implement efficient tools (in the sense that they are able to handle programs of a meaningful size), and to move beyond simple verification and towards automatic correction of existing code. Several verification tools were developped these last few years to verify properties of higher order recursive schemes. In this project we have adopted a technique whereby a program scheme is transformed into a finite state-space machine called a collapsible pushdown automaton. This intermediate step allows to harness the rich theory surrounding finite and infinite automata.
The AMIS project succeeded in implementing a program scheme verification tool called C-Shore. This tool performs comparably to existing model checkers and can handle programs of about 50 lines of code. We were therefore able to validate our finite automata-based approach. We moreover contributed to the surrounding theory by proposing a way to move from the verification of programs to their synthesis based on given specifications.
An initial aim of our work was to develop a suitable input language for C-SHORe. This language would ideally have been closer to a real-world programming language than recursion schemes and would have contained natural inter-translations with recursion schemes.
However, except for small modifications to C-SHORe to support recursion schemes with case statements], we have not investigated this avenue in detail.
The study of input languages, thus, is a pressing avenue of future research.
Finally, although we have shown that the saturation algorithm generalises to concurrent collapsible pushdown systems, it still remains to develop practical algorithms that may be implemented as part of the C-SHORe tool. Following the same idea, we would also need to develop a module for synthesis of programs.
The theoretical and practical work leading to the C-Shore software was the object of around ten publications in renowned international conferences (such as ICALP, LICS or ICFP). Among notable theoretical contributions, we were able to simplify the transla
Among the first advances towards the automated verification of computer systems is the framework of /finite-state model-checking/, a set of techniques which appeared around 30 years ago and has now become widespread. Its specificity is to represent the system under study as a finite automaton, and to answer various queries on the system using standard algorithmic theory on finite graphs. This setting is particularly effective when analysing so-called /finite-state systems/, such as hardware circuits or certain security protocols, since this formal model is expressive enough to faithfully capture the essential behaviours of such systems.
More complex systems, for instance modern software, often exhibit several infinite or at least unbounded aspects, such as recursion, concurrency, the presence of unbounded data structures, and so on. In order to reason about such infinite-state systems, researchers have had to consider more general formal models able to at least partially take into account one or several of these infinite aspects.
In this proposal we focus on the treatment of recursion. In this context the simplest systems of interest are sequential recursive programs over bounded data domains, for instance C programs with recursive functions but without pointers. The behaviour of such programs is faithfully represented by pushdown automata, using the automaton's stack to represent the nesting of procedure calls. Several research teams elaborated on this idea to propose effective verification tools for recursive programs.
We wish to build up on the existing models for recursive sequential programs and explore the richer setting of higher-order recursion, where arguments of functions are no longer limited to values but can be functions themselves. Known abstract models for dealing with higher-order recursion include higher-order recursion schemes and higher-order pushdown automata or collapsible automata. Recent results over these objects have made this topic one of the main current trends in the community. However many important questions remain open.
Monsieur Arnaud Carayol (UNIVERSITE PARIS-EST MARNE LA VALLEE) – email@example.com
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
LIGM UNIVERSITE PARIS-EST MARNE LA VALLEE
Help of the ANR 103,160 euros
Beginning and duration of the scientific project: - 36 Months