Our life depends on software and systems using software. Nowadays, software is complex and, hence, error prone. In order to overcome this problem, we need methods for assisting the software development. This project addresses the challenging problem of program analysis by developing rigorous mathematical techniques dealing with the logically complex parts of software. At this aim, we will use, refine and combine methods from satisfiability checking, graph neural networks and symbolic computation. These will make possible the analysis of software that is beyond the power of existing methods since advanced symbolic computation techniques (invariant theory) and graph neural networks combined with satisfiability checking (SAT/SMT solving) is not exploited in the state-of-the-art program analysis methods and tools. e are going to develop new theory and algorithms that detects the problem symmetries and similarities in family of problems by combining invariant theory, graph neural networks and SAT/SMT solving which, unlike state-of-the-art, would allow solving efficiently theoretically intractable problems. Our research project targets the analysis of complex software and follows three main research directions:
Contact: Mădălina ERAŞCU.