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

NEWS

Year 2024

• The paper Fast and Exact Synthesis of Application Deployment Plans using Graph Neural Networks and Satisfiability Modulo Theory (by Eduard Laitin and Mădălina Eraşcu) has been accepted at International Joint Conference on Neural Networks 2024 (IJCNN 2024), part of IEEE WCCI 2024 (IEEE Proceedings).
• Mădălina is serving as PC member of 33rd International Conference on Artificial Neural Networks (ICANN 2024), organized by Dalle Molle Institute for Artificial Intelligence Research (IDSIA USI-SUPSI) in Lugano, Switzerland in collaboration with AIDD and AiChemist Horizon MSCA projects; USI-SUPSI Campus Est, Via la Santa 1, 6962 Lugano-Viganello, Switzerland
• Mădălina is serving as a PC member for the 20th Artificial Intelligence Applications and Innovations (AIAI 2024), Ionian University, Corfu, Greece; June 27-30, 2024.
• The traffic sign recognition benchmark that we proposed for VNN-COMP 2023 received the outstanding benchmark award.

Year 2023

• Vlad is serving in the Artifact Evaluation Commettee of 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2024 April 6-13, 2024, Luxembourg Ville, Luxembourg.
• Mădălina participated at Dagstuhl Seminar 23401 on Automated mathematics: integrating proofs, algorithms and data, October 1-6, 2023, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik in Germany. The talk she gave and interaction with other participants was around understanding the road from symmetries to the symmetry breakers of the constraint optimzation problems which appear in deployment in the Cloud of component-based applications.
• The paper Benchmarking Local Robustness of High-Accuracy Binary Neural Networks for Enhanced Traffic Sign Recognition (by Andreea Postovan and Mădălina Eraşcu) is accepted at Working Formal Methods Symposium (FROM) 2023 (EPTCS proceedings). Presentation here.
• Mădălina is serving as a PC member for 19th European Dependable Computing Conference, Student Forum, KU Leuven, April 8-11 2024, Leuven, Belgium.
• In July, my Master students defended their theses in an excellent fashion:
  • Marcus Ilisie. A Symbiosis of Constraint Optimization, Symmetries and Symmetry Breaking for Scalable Cloud Deployment Problems
  • Eduard Laitin. Speeding Up the Deployment in the Cloud of Component-based Applications using Graph Neural Networks and SMT solving
  • Vlad Luca. SAGE - A Tool for Optimal Deployments in Kubernetes Clusters
  • Andreea Postovan. Binarized Neural Networks for Traffic Sign Recognition: Training and Verification
• Mădălina is serving as subreviewer for The 14th International Symposium on Frontiers of Combining Systems (FroCoS 2023), Czech Institute of Informatics, Robotics and Cybernetics (CIIRC) of the Czech Technical University in Prague (CTU), Czech Republic, September 20-22, 2023.
• The paper SAGE -A Tool for Optimal Deployments in Kubernetes Clusters (by Vlad Luca and Mădălina Eraşcu) is on arxiv.org. Also accepted at The 14th IEEE International Conference on Cloud Computing Technology and Science (IEEE CloudCom), December 4-6 2023 (IEEE Proceedings).
• The paper Automatic Deployment of Component-based Applications in the Cloud (short paper) appeared in the Proceedings of the 7th SC-Square Workshop co-located with the Federated Logic Conference 2022 (FLoC 2022) as a part of the 11th International Joint Conference on Automated Reasoning (IJCAR 2022), Haifa, Israel, August 12, 2022.
• Following our work on binarized neural networks for traffic signs reconition, we have sent benchmarks for assessing the local robustness of the trained models to VNN-COMP 2023. The trained models involve layers as binarized convolution (as provided by Larq library), max pooling, batch normalization and dense See all benchmarks in the competition here.
• Mădălina is serving as PC member of 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2023), LORIA, Nancy, France, for Logic Programming and Symbolic Computation Tracks and the Workshop on Theory of Smart Contracts and Applications (TOSCA).
• Mădălina is serving as PC member of 32nd International Conference on Artificial Neural Networks (ICANN 2023), School of Engineering of Democritus University of Thrace, Greece.
• The paper Architecturing Binarized Neural Networks for Traffic Sign Recognition (by Andreea Postovan and Mădălina Eraşcu) is on arxiv.org. Also accepted at as full paper for oral presentation at 32nd International Conference on Artificial Neural Networks (ICANN 2023) (Springer LNCS Proceedings).
• Mădălina will be giving a contributed talk at The Tenth Congress of Romanian Mathematicians June 30 - July 5, 2023, Pitesti, Romania at the Special Session Logic and applications. The congress is jointly organized by the Section of Mathematical Sciences of the Romanian Academy, the Romanian Mathematical Society, the Simion Stoilow Institute of Mathematics of the Romanian Academy, the Faculty of Mathematics and Computer Science of the University of Bucharest, and the University of Pitesti. Presentation here.
• We host EuroProofNet WG3 Program Verification meeting. See the webpage for more details.
• Mădălina will serve as PC member of 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2024 April 6-13, 2024, Luxembourg Ville, Luxembourg.

Year 2022

• Mădălina and Andreea will present in the departamental scientific seminar (December 7th, 6PM) about the Verification of Binarized Neural Networks. Presentation here.
• Mădălina will be serving as PC member of The 16th Conference on Intelligent Computer Mathematics (CICM 2023), September 4 - 8, 2023, Cambridge, UK.
• We were selected to pitch at Demo Day of ADRVest Accel, on November 11th. The main feedback was that we need to find our market and to define better our competitive advantage.
• Starting October 2022, Mădălina is serving as the Chair of WG3 (Program Verification) of the COST action EuroProofNet - European research network on digital proofs.
• Mădălina is invited speaker at Dagstuhl Seminar 23401 on Automated mathematics: integrating proofs, algorithms and data, October 1-6, 2023, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik in Germany
• Mădălina is serving as a Chair of the Doctoral Program of The 15th Conference on Intelligent Computer Mathematics (CICM 2022), September 19 - 23, 2022, Tbilisi, Georgia.
• Mădălina is serving as PC member of The 15th Conference on Intelligent Computer Mathematics (CICM 2022), September 19 - 23, 2022, Tbilisi, Georgia.
• Our research work has been selected in ADRVest Accel, the first accelerator supported by West Regional Development Agency - West RDA. Our goal will be to check the business opportunity of a SaaS solution for the automated planning/deployment of resources for businesses which want to move their component-based applications in the Cloud in order to reduce their costs, time and the faults of the planning/deployment.

Project Members (current and former)

• Mădălina Eraşcu, PI, Senior Researcher
• Adrian Craciun, Senior Researcher
• Ioan Luca Vlad, PhD Student Researcher
• Anda Leşeanu, Master Student Junior Researcher
• Andreea Postovan, Master Student Junior Researcher
• Ioan Luca Vlad, Master Student Junior Researcher
• Marcus Ilisie, Master Student Junior Researcher
• Eduard Laitin, Master Student Junior Researcher

Publications and Reports

• 2022 Annual Report

• 2023 Annual Report

• 2024 Final Report

Github Repository

https://github.com/SAGE-Project

Contact: Mădălina ERAŞCU.