Logic Engines as a Service

The world of symbolic reasoning engines and their applications at Microsoft, including impactful results and recent progress in the field. From SMT solvers to future developments in Z3, discover how these engines handle satisfiability, theorem proving, and more with algorithms, data structures, and heuristics. Delve into the powerful tools like Lean, used in checking Win8 and Office, with billions of constraints solved. Witness the evolution towards fixed points, interpolants, and nonlinear arithmetics, shaping the landscape of symbolic reasoning.

• Logic Engines
• Symbolic Reasoning
• Microsoft Research
• SMT Solvers
• Theorem Provers

marl_630 Follow

Uploaded on Feb 16, 2025 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Logic Engines as a Service Leonardo de Moura and Nikolaj Bj rner Microsoft Research

2. Satisfiability Solution/Model sat, ? =1 8,? =7 ?2+ ?2< 1 ??? ?? > 0.1 8 ?2+ ?2< 1 ??? ?? > 1 unsat, Proof Is execution path P feasible? Is assertion X violated? W I T N E S S SAGE Is Formula F Satisfiable?

3. Theorem Prover Simplex Rewriting DPLL Superposition Z3 is a collection of Symbolic Reasoning Engines Congruence Closure Euclidean Solver Groebner Basis elimination

4. Symbolic Reasoning Engine Test Case Generation Verifying Compilers Model Based Testing Invariant Generation Type Checking Model Checking

5. Some Applications at Microsoft SAGE HAVOC Vigilante

6. Impact Used by many research groups TACAS paper (> 1500 citations) More than 35k downloads Ships with many popular systems Isabelle, Pex, SLAM/SDV, Solved more than 5 Billion constraints created by SAGE when checking Win8 and Office.

7. Results and Contributions Algorithms Decidable Fragments Data structures Heuristics

8. Recent Progress 1. Interpolants 2. Fixed Points Beyond Satisfiability 3. Strings 4.Nonlinear arith. New Engines Arithmetic, Bit-Vectors, Booleans, Arrays, Datatypes, Quantifiers

9. SMT solvers are popular

10. Future Z3 with objective functions (Bj rner) Leverage progress in MaxSAT for SMT Stochastic Local Search in Z3 (Wintersteiger) For hard feasibility problems from symbolic execution, floating points Lean: new theorem prover (de Moura) Powerful Dependent Type system, Higher-Order