Abstract:
Adopting set-based reasoning mostly is a must when it comes to automatic reasoning about infinite domains, and such reasoning naturally exploits the Boolean algebra structure of the powerset - or rather of computationally representable subsets of the powerset - of the domain. Various algorithmic approaches for reasoning about large or infinite domains have exploited this fact, like constraint logic programming, interval constraint propagation and Cleary's logical arithmetic, branch-and-bound methods, or abstract interpretation. The iSAT SAT-modulo-theory (SMT) solver family for undecidable fragments of arithmetic involving transcendental functions probably was historically the first one to exploit this Boolean algebra view on (interval-shaped) subsets of the reals and its similarity to the subsets of the Booleans factually manipulated by CDCL-style SAT solvers for a direct integration of arithmetic constraint solving and propositional SAT solvers. It thereby circumvents the traditional use of Boolean abstractions referring to theory atoms within the SAT-solving based manipulation of the Boolean connectives and of theory solvers external to the SAT-solving procedure.

Within the talk, we will explain the algorithmics underlying iSAT and related solvers, like dReal, will talk about extensions to richer logical settings beyond mere existential satisfiability checking, and demonstrate applications. For the latter, ranging from bounded model checking of hybrid systems and reachability analysis in arithmetic-dominated industrial C-code over stochastic hybrid systems to precise monitoring of temporal logic specifications under partial state observation via inexact sensors, we will show the pertinent reductions to SMT problems permitting their automation by arithmetic SMT solving. Finally, we will contemplate some ideas on exploiting SMT techniques for lifting machine learning from its current point-based status (w.r.t. training and test data) to set-based (being able to rigorously generalize finite sets of labelled training points to uncountably infinite training sets).

CV:
Martin Fränzle has been the Professor for Hybrid Systems within the Department of Computing Science at the University of Oldenburg since 2004 and for Foundations and Application of Systems of Cyber-Physical Systems since 2022. He holds a diploma and a doctoral degree in Computer Science from Kiel University and was Associate Professor (2002-2004) and Velux Visiting Professor (2006-2008) at the Technical University of Denmark (DTU), Dean of the School of Computing Science, Business Administration, Economics, and Law at Oldenburg, and recently the Vice President for Research, Transfer, and Digitalization at the University of Oldenburg. His research spans a scope from fundamental research, in particular dynamic semantics and decidability issues of formal models of cyber-physical systems, over technology development addressing tools for the modelling, automated verification, and synthesis of cyber-physical and human-cyber-physical system designs to applied research as well as technology transfer with automotive and railway industries as well as design-tool vendors, the latter being based on numerous industrial cooperation projects. Together with Bernd Becker from Albert-Ludwigs-Universität Freiburg, he has been the driving force behind the development of the iSAT arithmetic SAT-modulo-theory (SMT) solver family, whose tight integration of unified Boolean-algebra reasoning over the Booleans, the integers, and the reals boosted performance of SMT solving over non-linear arithmetic domains, leading to its industrial take-up and commercial availability.

Abstract:
Applying formal verification techniques for digital circuits and software is commonly used to ensure corrections of specific properties. At matched.io, we do not develop hardware chips but tackle the challenge of matching candidates and companies together while applying techniques from a completely different industry. This talk will introduce computational challenges for an upcoming feature of matched.io to boost jobs' and candidates' profiles and show solutions learned from formal verification.

CV:
Stefan is co-founder of matched.io and focuses on the human part of software engineering and is deeply interested in various technologies and software engineering methodologies. At matched.io, Stefan tries to make match-making as valuable and fast as possible. Stefan received a PhD in computer science in 2013 and worked in various companies - from startups to big cooperates.