Thursday, 21 September 2023
| 8:30 | Registration |
| 9:20 | Opening |
| 9:30 | Invited talk: Ulrich Kohlenbach Proof Mining: Foundations and Applications |
| 10:30 | Coffee break |
| 11:00 | Mircea Marin, Temur Kutsia, Cleo Pau, Mikheil Rukhaia Enumerating all maximal clique-partitions of an undirected graph |
| 11:30 | Mihai Prunescu Symmetric functions over finite fields |
| 12:00 | Gabriel Istrate, Romeo Negrea q-Overlaps in the Random Exact Cover Problem |
| 12:30 | Lunch |
| 14:00 | Invited talk: Alicia Villanueva Symbolic reasoning for the inference of specifications |
| 15:00 | David Nowak, Vlad Rusu While Loops in Coq |
| 15:30 | Coffee break |
| 16:00 | Dorel Lucanu Matching-Logic-Based Understanding of Polynomial Functors and their Initial/Final Models |
| 16:30 | Jan Tušil, Péter Bereczky, Dániel Horpácsi Matching Logic Proof Mode in Coq |
| 17:00 | Horațiu Cheval Translating Matching Logic proofs from Lean to Metamath |
| 17:30 | End |
| 18:30 | Symposium dinner – Institute for Logic and Data Science (Popa Tatu 18) |
Friday, 22 September 2023
| 9:30 | Invited talk: Radu Iosif Formal Verification in the Era of Self-Adapting Networks |
| 10:30 | Coffee break |
| 11:00 | Andreea Postovan, Mădălina Erașcu Benchmarking Local Robustness of High-Accuracy Binary Neural Networks for Enhanced Traffic Sign Recognition |
| 11:30 | Ștefan-Claudiu Susan, Andrei Arusoaie Identifying vulnerabilities in Smart Contracts using Interval Analysis |
| 12:00 | Flávio L. C. De Moura, Maria Julia Dias Lima A formalized extension of the substitution lemma in Coq |
| 12:30 | Lunch |
| 14:00 | Invited talk: Eugenio Omodeo A proof verifier rooted in Set Theory and its bottleneck |
| 15:00 | Alen Docef, Radu Negulescu, Mihai Prunescu Using Z3 to Verify Inferences in Fragments of Linear Logic |
| 15:30 | Coffee break |
| 16:00 | Bogdan Macovei A Parallel Dynamic Epistemic Perspective over Muddy Children Puzzle |
| 16:30 | Dafina Trufaș, Ioan Teodorescu, Denisa Diaconescu, Traian Florin Șerbănuță, Vlad Zamfir Asynchronous Muddy Children Puzzle |
Privacy-preserving Linear Computations in Spiking Neural P Systems | |
| 17:00 | Radu Traian Bobe, Florentin Ipate, Ionuț Mihai Niculescu Modelling and search-based testing of robot controllers using enzymatic numerical P systems |
| 17:30 | End |