LPAR-25 will feature the following invited talks:
Erika Ábrahám (RWTH Aachen University)
TITLE: On the Idea of Exploration-guided Satisfiability Checking
ABSTRACT: Satisfiability checking is a research area devoted to the development and implementation of algorithms for the automated satisfiability check of logical formulas. SAT solving for propositional logic became impressively powerful due to an elegant combination of a smart search space exploration and proof construction. This idea has been later generalized to quantifier-free first-order logic formulas over some theories, most notably quantifier-free real algebra, in the framework of the model constructing satisfiability calculus (MCSAT). Both approaches are based on the generalization of "wrong guesses" made by the exploration into pieces of a proof, which are collected and used to synthesize a global proof during the solving process. While being one of the currently best approaches, for large or complex formulas, a large number of "proof pieces" cause high effort for their processing and thus restrict scalability. Thus the question comes up whether there are ways to store such information in a more structured way, which requires lower costs for processing. This thought is taken up by the method of the cylindrical algebraic coverings, developed for the satisfiability check of conjunctions of polynomial constraints.In this talk, we will discuss the above ideas and methods, and highlight their relations and differences.
BIOGRAPHY: Erika Ábrahám was born in Hungary and moved to Germany to study Computer Science at the University of Kiel. She received her Ph.D. from the University of Leiden, the Netherlands in 2005, for her work on deductive proof systems for concurrent programs. As a postdoctoral researcher, she was active in different areas of formal methods at the University of Freiburg and at Forschungszentrum Jülich, before she became professor at RWTH Aachen University, Germany in 2008. Her research areas cover the development of algorithms and tools (solvers) for satisfiability checking, and formal methods for the synthesis and analysis of discrete, hybrid, and probabilistic systems.
Armin Biere (University of Freiburg)
TITLE: 30 Years of Faster and Faster SAT Solving
ABSTRACT: This talk expands on preliminary results on "The SAT Museum" presented at the POS'23 workshop and the Shonan Seminar in 2023 on "The Art of SAT". This effort is targeted towards preserving historical SAT solvers, by collecting and porting their source code to modern compilers and evaluating them on representative benchmark sets from SAT competitions on the same modern hardware. This allows us to compare historic and modern solvers in the same environment. Our experiments show that SAT solvers are getting faster and faster with observable quantum leaps every three to five years. We present this historical perspective, explain conjectures on the source of these quantum leaps and also discuss more recent controversial insights
BIOGRAPHY: Since August 2021 Professor Armin Biere is leading the Chair of Computer Architecture at the Albert-Ludwigs-University Freiburg in Germany after 17 years as head of the Institute for Formal Models and Verification at the Johannes Kepler University in Linz, Austria. Between 2000 and 2004 he held a position as Assistant Professor within the Department of Computer Science at ETH Zürich, Switzerland. In 1999 Biere was working for a start-up company in electronic design automation after one year as Post-Doc with Edmund Clarke at CMU, Pittsburgh, USA. In 1997 Biere received a Ph.D. in Computer Science from the University of Karlsruhe, Germany. His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking and related techniques with the focus on developing efficient SAT and SMT solvers. He is the author and co-author of more than 220 papers and served on the program committee of more than 160 international conferences and workshops. His most influential work is his contribution to Bounded Model Checking. Decision procedures for SAT, QBF and SMT, developed by him or under his guidance rank at the top many international competitions and were awarded 104 medals including 57 gold medals. He is a recipient of an IBM faculty award in 2012, received the TACAS most influential paper in the first 20 years of TACAS award in 2014, the HVC'15 award on the most influential work in the last five years in formal verification, simulation, and testing, the ETAPS 2017 Test of Time Award, the CAV Award in 2018, the IJCAI-JAIR 2019 Award, and the 1990s Most Influential Paper Award at DAC'23.
Joost-Pieter Katoen (RWTH Aachen University)
TITLE: Probabilistic Programs. Verified. Push-Button.
ABSTRACT: Probabilistic programs encode randomized algorithms, robot controllers, learning components, security mechanisms, and much more. They are however hard to grasp. Not only by humans, also by computers: checking elementary properties related to e.g., termination are "more undecidable" than for ordinary programs. Although this all sounds like a no-go for automated analysis, I will present some non-trivial analyses of probabilistic programs using push-button technology. Our techniques are all based on weakest precondition reasoning. We will address automated techniques for termination detection, run-time analysis, k-induction, and the synthesis of probabilistic loop invariants.
BIOGRAPHY: Joost-Pieter Katoen is a distinguished professor at RWTH Aachen University, leading the Software Modeling and Verification (MOVES) group. He is part-time affiliated to the University of Twente. His main research contributions are in model checking, concurrency theory, probabilistic programming, and formal semantics. His book Principles of Model Checking (with Christel Baier) is a bestseller in formal verification. He received numerous best paper awards and other honors, most recently the JCL Award 2023 in Dependable Computing. He is a member of the Academia Europaea, the Royal Holland Society of Sciences and Humanities (KHMW) and the NRW Academy of Science and Arts (2022). He received an honorary doctorate from Aalborg University (2017), and an ERC Advanced Grant on probabilistic programming foundations (2018). He is also an ACM Fellow (2020).
Kuldeep Meel (University of Toronto)
TITLE:
ABSTRACT:
BIOGRAPHY: Kuldeep Meel is an Associate Professor of Computer Science in the Department of Computer Science at the University of Toronto. His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of the 2022 ACP Early Career Researcher Award, the 2019 NRF Fellowship for AI, and was named AI's 10 to Watch by IEEE Intelligent Systems in 2020. His research program's recent recognitions include the 2023 CACM Research Highlight Award, 2022 ACM SIGMOD Research Highlight, IJCAI-22 Early Career Spotlight, Distinguished Paper Award at CAV-23, "Best Papers of CAV" (2020 and 2022) special issue in FMSD journal, Best Paper Award nominations at ICCAD-21 and DATE-23, 1st Place in Model Counting Competition (2020 and 2022). He is passionate about teaching, and most proud of being recipient of university-level Annual Teaching Excellence Awards in 2022 and 2023.