Loading presentation...

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

Independent Proof Reconstruction for Z3: An Overview

Z3 Special Interest Group Meeting; Microsoft Research Cambridge; 3 November, 2011
by

Tjark Weber

on 6 October 2013

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Independent Proof Reconstruction for Z3: An Overview

Independent Proof Reconstruction for Z3: An Overview
Tjark Weber
Z3 Special Interest Group Meeting
3 November, 2011
System Overview
Validation
Automation
Demo
LCF-style Theorem Proving
Theorems are implemented as an abstract data type.
There is a fixed number of constructor functions - one for each axiom/inference rule of higher-order logic.
More complicated proof procedures must be implemented by composing these functions.
Z3 uses about 34 different inference rules.
LCF-style Proof Reconstruction
Proof Structure
Proofs are directed acyclic graphs.
Each node corresponds to an inference step.
Children are premises of inferences. Leaves are axioms/assumptions.
A designated root note concludes .
Proofs can be checked by depth-first postorder traversal.
1. A single primitive inference/theorem instantiation.
2. Combinations of primitive inferences/theorem instantiations.
3. Automated proof procedures (e.g., for linear arithmetic).
4. Combinations of the above.
Combinations of Primitive Inferences
Avoiding Automated Proof Procedures
Combinations of primitive inferences
Instantiation of schematic theorems
Generalization wrt. background theories
Memoization
Speed-ups of up to 3 orders of magnitude!
Evaluation
Independent Proof Reconstruction for Z3: An Overview
http://www.cl.cam.ac.uk/~tw333/
SMT-LIB
LCF-style proof checking is feasible for Z3. It scales to large formulas and proofs with millions of inferences.

Naive solutions are slow - an efficient implementation is crucial! Also, some ITP kernel optimizations were necessary.

Our integrations provide a high degree of automation in Isabelle and HOL4, enable new applications, and provide high assurance for Z3's results.
Conclusions
Certificate validation in Isabelle/HOL is about 19 times slower than proof search with Z3.
Timeouts are due to theory reasoning; Z3's proofs are not detailed enough.
75% of SMT-LIB problems are checked successfully!
Interactive Theorem Proving
A theorem prover is a computer program to prove theorems.
Given a precise description of a system, and a formal specification of its intended behavior, we obtain a computer-checked proof that the system meets its specification.
Lemma “ ”
by smt
[ITP 2010, CPP 2011]
[ITP 2010]
Interactive Theorem Proving
Expressivity
Automation
SMT
ITP Integration
LCF-style theorem provers are ...
generic
sound
powerful
e.g., based on higher-order logic
provided their kernel is correct
term rewriting, arithmetic, ...
Our Requirements
Cutting-edge performance
Proofs
Documentation
Linux version
Responsive developers
Short release cycles
In-memory API
Models
Wish List
Source code access
More detailed proofs
More expressivity
(rewrite, th-lemma)
(lambdas, higher-order logic)
Proofs
... should be easy (and fast) to generate.
... should be easy (and fast) to check.
Z3
User
AUFLIA
AUFLIRA
QF_UFLIA
QF_UF
QF_UFLRA
Profiling
Fewer bugs
(automated testing?)
Z3
Full transcript