🗊Презентация SAT and model checking

Категория: Математика
Нажмите для полного просмотра!
SAT and model checking, слайд №1SAT and model checking, слайд №2SAT and model checking, слайд №3SAT and model checking, слайд №4SAT and model checking, слайд №5SAT and model checking, слайд №6SAT and model checking, слайд №7SAT and model checking, слайд №8SAT and model checking, слайд №9SAT and model checking, слайд №10SAT and model checking, слайд №11SAT and model checking, слайд №12SAT and model checking, слайд №13SAT and model checking, слайд №14SAT and model checking, слайд №15SAT and model checking, слайд №16SAT and model checking, слайд №17SAT and model checking, слайд №18SAT and model checking, слайд №19SAT and model checking, слайд №20SAT and model checking, слайд №21SAT and model checking, слайд №22SAT and model checking, слайд №23SAT and model checking, слайд №24
Скачать
Вы можете ознакомиться и скачать презентацию на тему SAT and model checking. Доклад-сообщение содержит 24 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.

Слайды и текст этой презентации

Слайд 1


SAT and Model Checking
Описание слайда:
SAT and Model Checking

Слайд 2


Bounded Model Checking (BMC) A.I. Planning problems: can we reach a desired state in k steps? Verification of safety properties: can we find a bad state in k steps? Verification: can we find a counterexample in k steps ?
Описание слайда:
Bounded Model Checking (BMC) A.I. Planning problems: can we reach a desired state in k steps? Verification of safety properties: can we find a bad state in k steps? Verification: can we find a counterexample in k steps ?

Слайд 3


What is SAT?
Описание слайда:
What is SAT?

Слайд 4


BMC idea
Описание слайда:
BMC idea

Слайд 5


BMC idea (cont’d)
Описание слайда:
BMC idea (cont’d)

Слайд 6


Safety-checking as BMC
Описание слайда:
Safety-checking as BMC

Слайд 7


Example: a two bit counter
Описание слайда:
Example: a two bit counter

Слайд 8


Example: another counter
Описание слайда:
Example: another counter

Слайд 9


What BMC with SAT Can Do All LTL ACTL and ECTL In principle, all CTL and even mu-calculus efficient universal quantifier elimination or fixpoint computation is an active area of research
Описание слайда:
What BMC with SAT Can Do All LTL ACTL and ECTL In principle, all CTL and even mu-calculus efficient universal quantifier elimination or fixpoint computation is an active area of research

Слайд 10


How big should k be? For every model M and LTL property  there exists k s.t. The minimal such k is the Completeness Threshold (CT)
Описание слайда:
How big should k be? For every model M and LTL property  there exists k s.t. The minimal such k is the Completeness Threshold (CT)

Слайд 11


How big should k be? Diameter d = longest shortest path from an initial state to any other reachable state. Recurrence Diameter rd = longest loop-free path. rd ¸ d
Описание слайда:
How big should k be? Diameter d = longest shortest path from an initial state to any other reachable state. Recurrence Diameter rd = longest loop-free path. rd ¸ d

Слайд 12


How big should k be? Theorem: for Gp properties CT = d
Описание слайда:
How big should k be? Theorem: for Gp properties CT = d

Слайд 13


How big should k be? Theorem: for Fp properties CT= rd
Описание слайда:
How big should k be? Theorem: for Fp properties CT= rd

Слайд 14


A basic SAT solver Given  in CNF: (x,y,z),(-x,y),(-y,z),(-x,-y,-z)
Описание слайда:
A basic SAT solver Given  in CNF: (x,y,z),(-x,y),(-y,z),(-x,-y,-z)

Слайд 15


SAT and model checking, слайд №15
Описание слайда:

Слайд 16


DPLL-style SAT solvers
Описание слайда:
DPLL-style SAT solvers

Слайд 17


The Implication Graph
Описание слайда:
The Implication Graph

Слайд 18


Resolution
Описание слайда:
Resolution

Слайд 19


Conflict clauses
Описание слайда:
Conflict clauses

Слайд 20


Conflict Clauses (cont.) Conflict clauses: Are generated by resolution Are implied by existing clauses Are in conflict with the current assignment Are safely added to the clause set
Описание слайда:
Conflict Clauses (cont.) Conflict clauses: Are generated by resolution Are implied by existing clauses Are in conflict with the current assignment Are safely added to the clause set

Слайд 21


Generating refutations Refutation = a proof of the null clause Record a DAG containing all resolution steps performed during conflict clause generation. When null clause is generated, we can extract a proof of the null clause as a resolution DAG.
Описание слайда:
Generating refutations Refutation = a proof of the null clause Record a DAG containing all resolution steps performed during conflict clause generation. When null clause is generated, we can extract a proof of the null clause as a resolution DAG.

Слайд 22


Unbounded Model Checking A variety of methods to exploit SAT and BMC for unbounded model checking: Completeness Threshold k - induction Abstraction (refutation proofs useful here) Exact and over-approximate image computations (refutation proofs useful here) Use of Craig interpolation
Описание слайда:
Unbounded Model Checking A variety of methods to exploit SAT and BMC for unbounded model checking: Completeness Threshold k - induction Abstraction (refutation proofs useful here) Exact and over-approximate image computations (refutation proofs useful here) Use of Craig interpolation

Слайд 23


Conclusions: BDDs vs. SAT Many models that cannot be solved by BDD symbolic model checkers, can be solved with an optimized SAT Bounded Model Checker. The reverse is true as well. BMC with SAT is faster at finding shallow errors and giving short counterexamples. BDD-based procedures are better at proving absence of errors.
Описание слайда:
Conclusions: BDDs vs. SAT Many models that cannot be solved by BDD symbolic model checkers, can be solved with an optimized SAT Bounded Model Checker. The reverse is true as well. BMC with SAT is faster at finding shallow errors and giving short counterexamples. BDD-based procedures are better at proving absence of errors.

Слайд 24


Acknowledgements
Описание слайда:
Acknowledgements

Скачать

Теги SAT and model checking
Похожие презентации
Mypresentation.ru
Загрузить презентацию