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.
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
Logic Engines as a Service Leonardo de Moura and Nikolaj Bj rner Microsoft Research
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?
Theorem Prover Simplex Rewriting DPLL Superposition Z3 is a collection of Symbolic Reasoning Engines Congruence Closure Euclidean Solver Groebner Basis elimination
Symbolic Reasoning Engine Test Case Generation Verifying Compilers Model Based Testing Invariant Generation Type Checking Model Checking
Some Applications at Microsoft SAGE HAVOC Vigilante
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.
Results and Contributions Algorithms Decidable Fragments Data structures Heuristics
Recent Progress 1. Interpolants 2. Fixed Points Beyond Satisfiability 3. Strings 4.Nonlinear arith. New Engines Arithmetic, Bit-Vectors, Booleans, Arrays, Datatypes, Quantifiers
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
