Logic Engines as a Service

Logic Engines as a Service
Slide Note
Embed
Share

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

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.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

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.

E N D

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

More Related Content