SYMCAR
Financiado
Symbolic Computation and Automated Reasoning for Program Analysis
Individuals, industries, and nations are depending on software and systems using software. Automated approaches are needed to eliminate tedious aspects of software development, helping software developers in dealing with the incre...
Individuals, industries, and nations are depending on software and systems using software. Automated approaches are needed to eliminate tedious aspects of software development, helping software developers in dealing with the increasing software complexity. Automatic program analysis aims to discover program properties preventing programmers from introducing errors while making changes and can drastically cut the time needed for program development.
This project addresses the challenge of automating program analysis, by developing rigorous mathematical techniques analyzing the logically complex parts of software. We will carry out novel research in computer theorem proving and symbolic computation, and integrate program analysis techniques with new approaches to program assertion synthesis and reasoning with both theories and quantifiers. The common theme of the project is a creative development of automated reasoning techniques based on our recently introduced symbol elimination method. Symbol elimination makes the project challenging, risky and interdisciplinary, bridging together computer science, mathematics, and logic.
Symbol elimination will enhance program analysis, in particular by generating polynomial and quantified first-order program properties that cannot be derived by other methods. As many program properties can best be expressed using quantified formulas with arithmetic, our project will make a significant step in analyzing large systems. Since program analysis requires reasoning in the combination of first-order logic and theories, we will design efficient algorithms for automated reasoning with both theories and quantifiers. Our results will be supported by the development of world-leading tools supporting symbol elimination in program analysis.
Our project brings breakthrough approaches to program analysis, which, together with other advances in the area, will reduce the cost of developing safe and reliable computer systems used in our daily life.
ver más
Duración del proyecto: 72 meses
Fecha Inicio: 2015-06-30
Fecha Fin: 2021-06-30
Fecha Fin: 2021-06-30
Línea de financiación: concedida
El organismo H2020 notifico la concesión del proyecto el día 2021-06-30
Línea de financiación objetivo
El proyecto se financió a través de la siguiente ayuda:
ERC-StG-2014:
ERC Starting Grant
Cerrada
hace 10 años
Presupuesto
El presupuesto total del proyecto asciende a
2M€
Líder del proyecto
TECHNISCHE UNIVERSITAET WIEN
No se ha especificado una descripción o un objeto social para esta compañía.
Perfil tecnológico
TRL
4-5
Perfil tecnológico
TRL
4-5
437.49K€ |
Participante