ICTAC 2026
November 9-15, 2026
Bariloche
Bariloche
RWTH Aachen University
Erika Abraham graduated at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the development and application of deductive proof systems for concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the development and application of SAT and SMT solvers. Currently she is professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.
Theory and Applications of Satisfiability Modulo Theories (SMT) solving
SMT (Satisfiability Modulo Theories) solving is a technology for the fully automated solution of logical formulas. SMT solvers can be used as general-purpose off-the-shelf tools. Due to their impressive efficiency, they are nowadays frequently used in a wide variety of applications. A typical application encodes real-world problems as logical formulas, whose solutions can be decoded to solutions of the real-world problem. Besides its unquestionable practical impact, SMT solving has another great merit: it inspired truly elegant ideas, which do not only enable the construction of efficient software tools, but provide also interesting theoretical insights. In this talk, we give an introduction to the mechanisms of SAT and SMT solving, discuss some interesting ideas in the underlying algorithms, and illustrate the usage of SMT solvers on a some application examples.
CONICET and Universidad Nacional de Río Cuarto, Argentina
Guangdong Technion-Israel Institute of Technology, China
Nazareno Aguirre is a Full Professor at the University of Rio Cuarto, Argentina, and a Research Scientist at Argentina's National Council for Scientific and Technical Research (CONICET). He is also a Visiting Professor at Guangdong Technion Israel Institute of Technology, Shantou, China. His current research interests relate to the problem of guaranteeing software correctness and helping produce quality software, mostly via techniques for program specification, automated testing, and program verification, with formal underpinnings. Nazareno Aguirre's research has been published in top-tier software engineering conferences and journals. He regularly serves on program committees of premier software engineering conferences and is currently an Associate Editor of IEEE Transactions on Software Engineering.
Formal Analysis of Software Requirements: Boundary Conditions and Tools to Handle Them
The analysis of software requirements is a crucial activity, as identifying issues early in software development is more effective and less costly than addressing them after they have propagated into design and implementation. While some requirements problems, such as direct contradictions, are relatively easy to identify, others are far more subtle. In particular, if the requirements are organized as a set of system goals, these may overall be compatible (i.e., jointly satisfiable), yet under specific circumstances, called boundary conditions, it may be impossible to simultaneously satisfy all requirements. Identifying, assessing, and resolving these situations are core challenges in requirements engineering. This talk traces the evolution of our work on this problem, from automated conflict detection in Linear-Time Temporal Logic (LTL) formal requirements specifications, through scalability-driven adoptions of genetic algorithms and approximate model counting, to a fuzzing technique that turns our analysis tools into objects of analysis themselves.
Universidad Católica de Chile
Full Professor at Pontificia Universidad Católica de Chile, where he also acts as Director of the Institute for Mathematical and Computational Engineering. Ph.D. in Computer Science from the University of Toronto, Canada. Recently, he served as Deputy Director of the Millennium Institute for Foundational Research on Data (IMFD Chile). He is the author of more than 80 technical papers, has chaired ICDT 2019 and ACM PODS 2022, and is currently a member of the editorial committee of Logical Methods in Computer Science. From 2011 to 2014 he was the editor of the database theory column of SIGMOD Record. His areas of interest are database theory, logic in computer science, and the emerging relationship between these areas and machine learning.
The Role of Logic in Advancing Machine Learning: Three Case Studies
I present three case studies from my collaborative research that highlight the essential role of logic in enhancing our understanding of modern machine learning architectures. The first two examples focus on the expressive capabilities of two prominent architectures: Transformers, which have revolutionized NLP applications, and Graph Neural Networks, a leading approach for classifying graph-structured data. We employ temporal logic techniques to analyze the properties that Transformers can recognize, and modal logics to examine the properties discernible by Graph Neural Networks. The third example addresses the pursuit of explainable AI, demonstrating how first-order logic can be used to design languages that declare, evaluate, and compute explanations for decisions made by machine learning models.