Symbolic computing methods, including abstract interpretation, symbolic execution, theorem proving, model building and model checking, are integrated in tools to debug systems in early development stages and synthesize them from user requirements. Each method has strengths and weaknesses, while the ever increasing growth in the diversity and complexity of software and hardware systems makes automated analysis and synthesis more needed than ever in order to keep the quality/cost curve sustainable. This project develops new synergies between abstract interpretation and automated reasoning, enabling the reasoners to benefit from abstractions, and analyzers/synthesizers from proofs, models, interpolants, provided by the reasoners. While from a technical point of view the project is concerned with applications within computing itself, the ubiquitous role of software and hardware systems in contemporary life makes its impact on the economy and society profound and long lasting.
This projects fits in with all three directions of Horizon 2020: (1) Excellent science, (2) Competitive industry, and (3) Better
society. For (1), the challenge of reliable software and trusted components has been recognized as one of the great challenges for science at the dawn of the XXI century. For (2), the software verification method of choice in industry today is testing, which is very expensive (79bn euro world-wide in 2010) and expected to cost even more in the future. Verification, analysis and synthesis of software by symbolic methods does not seek to replace testing, but complement it and enhance it, reducing development cost. This is especially relevant for Italy and Europe, because the vast majority of our enterprises are medium or small, and therefore less well equipped financially to bear the cost of testing, which propagates from software production to all other branches of the economy. Beyond ICT, increasing the reliability, safety and efficiency of software and hardware systems has impact on key industrial and service sectors including energy, transportation, banking, and health. This leads to (3), where the impact is even broader, as software affects life styles (e.g., inter-personal communication, social networks), education at all levels, public information, political participation (e.g., electronic voting systems), personal management (e.g., internet banking), and everyday chores. The quality of life, freedom and democracy that we enjoy depend also on software.
The complexity, variety, size and pervasiveness of software are such, that no single approach is expected to be good enough on its own and in general. An increasingly wide-spread vision, shared by this project, is to have a pipeline of tools, where technologies of increasing cost are applied to problems of increasing difficulty. Abstract interpretation trades precision for efficiency, and therefore is applied early. Reasoning strives for efficiency while preserving completeness, and therefore is applied late in the pipeline. The spectacular progress in theorem proving, model building and constraint solving, known as SMT big bang, leads us to short-circuit the pipeline, to let abstract interpretation and reasoning work together. This vision informs our research towards five objectives:
1. Theorem proving for automated invariant generation,
2. Automated termination analysis,
3. Metamorphic code analysis,
4. Abstraction-driven synthesis, and
5. Trace just-in-time compilation.
Automated invariant generation relieves programmers from annotating code and enables end users to participate in program generation by providing merely examples. Termination is fundamental for correctness, while metamorphic code analysis is used to detect malicious software (malware). Abstraction-driven synthesis is applied to automate the synchronization of concurrent programs, while trace just-in-time compilation is key to optimize programs in languages used in web programming.