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

Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL

CPP 2011; Kenting, Taiwan; 8 December, 2011
by

Tjark Weber

on 3 October 2013

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL

Tjark Weber
CPP 2011
8 December, 2011
System Overview
Validation
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.
Z3: Inference Rules
Z3: 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
.
Evaluation
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
SMT-LIB
Conclusions
Proofs
... should be easy (and fast) to generate.
... should be easy (and fast) to check.
Reconstruction of Z3's Bit-Vector Proofs in
HOL4 and Isabelle/HOL
Sascha Böhme
Anthony Fox
Thomas Sewell
http://user.it.uu.se/~tjawe125/
Automation
Motivation
Related Work
Arrays
Bit-Vectors
Core
Ints
Reals
Reals_Ints
SMT-LIB's Theory of Fixed-Width Bit-Vectors
sorts
BitVec m
, for every m > 0

bit-vector constants, e.g.,
#b0

logical operations (
bvnot
,
bvand
,
bvor
, ...)

arithmetic operations (
bvneg
,
bvadd
,
bvmul
, ...)

concatenation, extraction, shift operations, etc.
Bit-Vectors in Higher-Order Logic
SMT-LIB
HOL
Translating bit-vector
terms
between SMT-LIB and HOL is relatively straightforward.
bit-vector sorts
bit-vector constants
logical operations
arithmetic operations
...
bit-vector types
bit-vector literals
logical operations
arithmetic operations
...
Only 2 rules involve bit-vector reasoning.
rewrite
th-lemma-bv
equality reasoning about interpreted functions
Proof Reconstruction for rewrite and th-lemma-bv
Schematic theorems
arbitrary theory-specific lemmas
74% of SMT-LIB problems are checked successfully!

Proof reconstruction is an order of magnitude faster than LCF-style bit-blasting.

Proof generation with Z3 is up to two orders of magnitude faster than proof reconstruction.

Timeouts are due to theory reasoning; Z3's proofs are not detailed enough.
Theorem memoization
Strategy selection
rewrite
th-lemma-bv
Z3 timeout/error
Error
QF_AUFBV
Timeout
Success
QF_BV
QF_UFBV
Benchmarks
Profiling
th-lemma-bv
rewrite
other
% runtime
QF_AUFBV
QF_BV
QF_UFBV
Full transcript