SAGE: A Symbiosis of Satisfiability Checking, Graph Neural Networks and Symbolic Computation

  • Director: Mădălina Eraşcu
  • Funding Agency: UEFISCDI (PN-III-P1-1.1-TE-2021-0676)
  • Project Period: September 2022 - August 2024
  • Host Institution: West University of Timisoara

  • Project Overview

    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:

    1. Methods for symmetry breaking and for learning problems similarities
    2. Theory and algorithms
    3. Tools and evaluations


    Project Members

    External Colaborators

    Publications and Reports

    Github Repository

    Contact: Mădălina ERAŞCU.