See the schedule here
Abstract TBA
Bio:Dr. Leberre is professor in Lens, where he works on SAT solving and beyond with the SAT4j SAT solver in Java.
Abstract TBA
Bio:Dr. Rozier is working in Iowa State University. She works on various formal tools like MLTL that is used by the NASA Lunar Gateway Vehicle System Manager.
Abstract TBA
Bio:Dr. Fazekas is doing research at the TU Wien, after doing her PhD in Linz and doing a Research Fellow at the Simons Instute. One of her topics of research are deeper integration of SMT and SAT solving by providing external control.
Abstract TBA
Bio:Prof. Dr. Armin Biere is now in Freiburg after spending many years in Linz. He is very famous for his work on SAT solvers. As Karem Sakallah mentioned in a talk: The SAT Competition is a simple game. Many people submit a solver and at the end, Armin wins. He is also very active on Twitter, Mastodon, and various other social networks.
Abstract
Satisfiability Modulo Theories (SMT) is the problem of determining the
satisfiability of a first-order formula in a logical theory of interest. Typical
theories include various forms of arithmetic and of various data types such as
arrays, bit-vectors, strings, and so on. SMT solvers are highly efficient and
versatile systems specialized for this problem, widely used as backend engines
in many application domains.
However, when an application does not entirely fit the predefined theories,
quantifiers may be used to provide new axioms to complement them. SMT solvers
generally rely on various instantiation techniques to handle quantifiers,
increasingly reducing quantified problems to ground ones so that the efficient
theory procedures can be leveraged.
This lecture will cover the state of the art in instantiation techniques in SMT
solving, detailing and motivating different techniques and showing how they
complement each other.
Bio:Prof. Barbosa is one of the main developers of SMT solvers: during his PhD he worked on veriT in Nancy, during his postdoc in Iowa on CVC4, and now he works on cvc5, the successor of CVC4 (except for the writing of the solver name).
Abstract TBA
SummaryThis lecture gives an overview of the most used techniques for quantifier-free SMT solving, focusing on the CDCL(T) architecture and some important theory solvers.
Bio:Prof. Griggio is one of the developers of the SMT solver MathSAT, but is also involved in projects beyond SMT like the model checker nuXmv.
Abstract
Interfacing SMT Solvers using SMT-LIB and Python
This lecture will give an overview of two of the main ways to
interface SMT solvers: the standardized SMT-LIB format, and the (less
standardized, but very popular and useful) Python APIs provided by SMT
solvers like Z3 and cvc5. Aside from a brief introduction to SMT-LIB
and the APIs, most of the time will be allocated for exercises and
practical tasks, in which the participants will be guided to model and
solve problems from different domains using SMT solvers on their own
computers.
Bio:Prof. Rümmer from the University of Regensburg is interested in all things SMT and ATP, including provers for first-order logic, solvers for theories of strings, sequences, arithmetic, solvers for constrained Horn clauses, and various applications.
Partical:https://shorturl.at/vd5RK
Abstract Amazon Web Services (AWS) is a cloud computing services provider that has made significant investments in automated reasoning to check the correctness of its internal systems and to provide assurances to customers. We are using SAT and SMT solvers more than one billion times a day, both for "real-time" queries in customer security (checking security policies and verifying network protections), and also for large queries involving code and hardware reasoning that are at the limits of what can be feasibly solved by current solvers. Supporting reasoning at this scale and volume requires careful examination of the problems to be solved and a clear focus on operations to ensure our analyses are consistently trustworthy and performant. I will describe some lessons learned and offer some directions for the community that should allow us to scale further, increase trust, and solve the next billion queries a day.
Bio:He is working in of the big companies that uses SMT solver, although you might not expect: Amazon ("one billion SMT queries a day"). He works on SAT and SMT solving.
Abstract TBA
Summary An taste of theorem proving: what it is (not). First-order theorem proving. Challenges and approaches. The popular saturation paradigm. An outline of the superposition calculus. A sketch of Vampire.
Bio:Dr. Rawson is one of the Vampire maintainers, so he moved from Manchester to work in Vienna now. When he is not attacking other solvers at yearly CASC competitions, he works on adding ML to automated reasoning.
Title Logic of Autonomous Dynamical Systems
Abstract This course highlights some of the most fascinating aspects of the logic of dynamical systems which constitute the foundation for developing cyber-physical systems (CPS) such as robots, cars and aircraft with the mathematical rigor that their safety-critical nature demands. Differential dynamic logic (dL) provides an integrated specification and verification language for dynamical systems, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations. In dL, properties of the global behavior of a dynamical system can be analyzed solely from the logic of their local change without having to solve the dynamics. In addition to providing a strong theoretical foundation for CPS, differential dynamic logics as implemented in the KeYmaera X prover have been instrumental in verifying many applications, including the Federal Aviation Administration's Airborne Collision Avoidance System ACAS X, a train control system for the Federal Railroad Administration, automotive systems, mobile robot navigation, and a surgical robotic system for skull-base surgery. dL is the foundation to provable safety transfer from models to CPS implementations and is also the key ingredient behind autonomous dynamical systems for Safe AI in CPS. References: André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. DOI:10.1007/978-3-319-63588-0 André Platzer. Logics of dynamical systems. LICS, 2012: 13-24. DOI:10.1109/LICS.2012.13
Bio:Prof. Dr. Platzer works at the KIT in Karlsruhe, where he is the Alexander von Humboldt Professor for cyber-physical systems, after being in Carnegie Mellon University for several years.
Abstract Automated Reasoning -- Core Algorithms and Data Structures
We will look at some core concepts shared by nearly all modern
automated theorem provers and related systems -- terms, substitutions,
unification, matching, as well as their applications, including
paramodulation/superposition, rewriting, and subsumption. I will
present actual code examples from PyRes and E, and discuss some
implementation details.
We will then also attempt to develop a new, unification-based clause
selection heuristic for E, and evaluate if it is a useful contribution
to the portfolio of strategies.
Participants are encouraged to bring a laptop with a UNIX/Linux style
C development system, and/or a recent Python-3 installation for the
practical work.
Practical Please download PyRes by doing git clone https://github.com/eprover/PyRes.git and E 3.2 from here
Bio:Prof. Dr. Schulz is a professor in Stuttgart. He is very famous for his E prover, where each version is named after some tea.
TitleProof checking in a verified way
Abstract TBA
Summary In a first part, I will present proof checking of automated solvers inside proof assistants: interest, history, approaches, results, ... The second part will be an interactive tutorial focusing on reusing SMTCoq's certified proof checker for checking one's proofs
Bio:Dr. Keller is Associate Professor in Paris (Université Paris-Saclay), where she works on various formalization in Coq or tools like SMTCoq that replays proof of SMT solvers in Coq to make sure that the proofs are correct.
Abstract TBA
Bio:He is a senior lecturers in London, where he works a term rewriting including higher order, sometimes creating benchmarks for SAT/SMT/AR.
Title Proof complexity and SAT solving
Abstract This talk is intended to give an overview of proof complexity and connections to Boolean satisfiability (SAT) solving. The focus will be on proof systems (and corresponding algorithms) such as resolution (DPLL and conflict-driven clause learning), Nullstellensatz and polynomial calculus (linear algebra and Gröbner basis computations), and cutting planes (pseudo-Boolean solving and 0-1 integer linear programming). Time permitting, we will also discuss briefly proof systems such as Sherali-Adams and sums of squares (linear programming and semidefinite programming hierarchies), stabbing planes (0-1 ILP), and extended resolution (SAT pre- and inprocessing).
Bio: Jakob Nordström is a professor at the University of Copenhagen, Denmark, with a side affiliation at Lund University on the Swedish side on the Oresund Bridge. He started his research career in computational complexity theory, but these days his activities also include (in addition to frequent, long train commutes) work on how to leverage complexity theory to build more efficient combinatorial solvers and how to develop proof logging methods for applications such as SAT solving, SAT-based optimization, graph solving, constraint programming, and integer linear programming using the VeriPB tool.