UnRAVeL-Ringvorlesung: Erika Àbrahám: Building Bridges between Symbolic Computation and Satisfiability Checking

Donnerstag, 13. April 2023, 12:30 Uhr

Ort: Informatikzentrum, Geb. E2, Erdgeschoss, B-IT-Raum 5053.2.

Vortragende: Erika Àbrahám

 

Abstract: 

The use of advanced methods to solve practical and industrially relevant problems by computers has a long history. Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems. More recent developments in the area of Satisfiability Checking started to tackle similar problems but with different algorithmic and technological solutions. Though both communities have made remarkable progress in the last decades, they need to be further strengthened to tackle practical problems of ever increasing size and complexity. Their separate tools (computer algebra systems and SMT solvers) are urgently needed to address prevailing problems having a direct effect on our society. For example, Satisfiability Checking is an essential backend for assuring the security and the safety of computer systems. In various scientific areas, Symbolic Computation is able to deal with large mathematical problems far beyond the scope of pencil and paper solutions. Until recently, the two communities have been largely disjoint and unaware of the achievements of one another, despite there being strong reasons for them to discuss and collaborate, since they share many central interests. Researchers from these two communities rarely interacted, and also their tools lack common, mutual interfaces for unifying their strengths. As said, until recently...