LPAR-24 will feature the following invited talks:
Konstantin Korovin, The University of Manchester, United Kingdom
TITLE: From Instantiation to Superposition with a Touch of Machine Learning
ABSTRACT:
Quantified first-order logic provides an experssive formalism that can beused to define various theories, data structures, systems and invariantswith applications ranging from mathematics to verification of hardware andsoftware. Efficient reasoning in quantified first-order logic is an ongoingquest with many approaches and provers such as Vampire, E, SPASS andiProver from the ATP side, and CVC5, Z3 and Yices from the SMT side. Inthis talk we will overview methods behind iProver, focusing on recentdevelopments. iProver started as an instantiation-based prover wherequantified first-order reasoning is combined with efficient SAT and SMTsolvers and recently has been extended with superposition,abstraction-refinement and machine learning for parameter optimisation andpremise selection. We also extended superposition itself with several novelredundancy elimination such as ground joinability, encompassmentdemodulation and connectedness, extending simplifications from theKnuth-Bendix completion to full first-order reasoning. These methods areapplicable to general quantified first-order theorem proving and we hopethat they will find their way into other systems.
BIOGRAPHY: Konstantin Korovin is a Senior Lecturer at the University ofManchester, UK.Previously, Konstantin was a Royal Society University Research Fellow atthe University of Manchester and a post-doc at the Max-Planck InstituteSaarbrucken. He obtained his PhD from the University of Manchester, UK, forwhich he received the Ackemann Award by The European Association forComputer Science Logic. Konstantin's main research interests include:automated theorem proving, verification, non-linear constraint solving andcombining reasoning with machine learning.
Mauricio Ayala-Rincón, Universidade de Brasília, Brazil
TITLE: Formalization of Algebraic Theorems in PVS
ABSTRACT: This talk will present extensions on the theory "algebra" from the NASA/PVSlibrary on formal developments for the Prototype Verification System PVS. Wewill discuss our approach to formalizing theorems of the ring theory and how itis applied to specific algebraic structures. As cases of study, we will presentour recent formalizations on (abstract) Euclidean Domains and Quaternions.Moreover, we will show how a general verification of Euclid's division algorithmcan be specialized to verify this algorithm in specific Euclidean Domains andhow the abstract formalization of Quaternions can be parameterized to deal withthe structure of Hamilton's Quaternions.
BIOGRAPHY: Mauricio Ayala-Rincón is a full Professor in Computer Science and Mathematics at the Universidade de Brasília. After finishing his Ph.D. at the Universität Kaiserslautern, he worked on the dissemination of rewriting techniques, formal methods, and applications in South America, maintaining cooperation with researchers at institutions such as PUC Rio, Karlsruhe Institute für Technologie, Heriot-Watt University, ICASE/NIA-NASA LaRC Formal Methods, UFG, UFCat,Universidad de Buenos Aires, Universidad Nacional de Quilmes, King's College London, and the Universidade Nacional de Colombia - sede Manizales. In addition, he served as a steering committee member of several workshops and conferences, such as LSFA, RTA, FSCD, UNIF, IWC, IWR, and ITP, and is a member of the IFIP WG1.6 in Rewriting. His current research interests focus on nominal equational reasoning, the formalization of algebraic theories, and the automation of termination.
Marijn Heule, Carnegie Mellon University, USA
TITLE: Computer-aided Mathematics: Successes, Advances, and Trust
ABSTRACT: Progress in satisfiability (SAT) solving has made it possible to determine the correctness of complex systems and answer long-standing open questions in mathematics. The SAT-solving approach is completely automatic and can produce clever though potentially gigantic proofs. We can have confidence in the correctness of the answers because highly trustworthy systems can validate the underlying proofs regardless of their size. We demonstrate the effectiveness of the SAT approach by presenting some successes, including the solution of the Boolean Pythagorean Triples problem, computing the fifth Schur number, and resolving the remaining case of Keller’s conjecture. Moreover, we constructed and validated proofs for each of these results. The second part of the talk focuses on notorious math challenges for which automated reasoning may well be suitable. In particular, we discuss advances in applying SAT-solving techniques to the Hadwiger-Nelson problem (chromatic number of the plane), optimal schemes for matrix multiplication, and the Collatz conjecture.
BIOGRAPHY: Marijn Heule is an Associate Professor at Carnegie Mellon University and received his PhD at Delft University of Technology (2008). His contributions to automated reasoning have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning SAT solvers and his preprocessing and proof-producing techniques are used in many state-of-the-art solvers. Marijn won multiple best paper awards at international conferences, including at SAT, CADE, IJCAR, TACAS, HVC, and IJCAI-JAIR. He is one of the editors of the Handbook of Satisfiability. This 900+ page handbook has become the reference for SAT research.
Roderick Bloem, Graz University of Technology, Austria
TITLE: Side Channel Secure Software
ABSTRACT: We present a method to reason about the security of masked software against power side channel attacks. Masking is a technique to hide secrets by duplication and addition of randomness. One of the reasoning methods that we will use is the Fourier expansion of Boolean functions to find correlations between variables and secrets. It turns out that reasoning about software alone is not enough to ensure correctness. Instead, we have to look at the detailed implementation of the CPU on which it executes. We consider the IBEX RISC-V processor, find vulnerabilities, and use our results to make the CPU more secure.
BIOGRAPHY: Roderick Bloem received his M.Sc. degree in Computer Science from Leiden University, the Netherlands, in 1996. He got his Ph.D. degree in Computer Science from the University of Colorado at Boulder in 2001. From 2002 until 2008, he was an Assistant at Graz University of Technology, Graz, Austria. From 2008, he has been a full professor of Computer Science at the same university. He is a co-editor of the Handbook of Model Checking and has published over 100 peer-reviewed papers in formal verification, reactive synthesis, Safe AI, and security. He lead the Austrian National Research Network on Rigorous Systems Engineering and has served as PC chair for events including the Computer Aided Verification conference and Formal Methods in Computer Aided Design. He's the head of the CS department, but not for much longer.