Avoiding state space explosion in model checker

➤ Gửi thông báo lỗi ⚠️ Báo cáo tài liệu vi phạm

Loại tài liệu: PDF

Số trang: 45 Trang

Tài liệu: ✅ ĐÃ ĐƯỢC PHÊ DUYỆT

TẢI VỀ

Nội dung chi tiết: Avoiding state space explosion in model checker

Avoiding state space explosion in model checker

VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF

Avoiding state space explosion in model checker INFORMATION TECHNOLOGYHanoi - 2014VIETNAM NATIONAL UNIVERSITY, HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBIT PHI DIEPAVOIDING STATE-SPACE EXPLOSIO

N IN MODEL-CHECKERMajor: Computer scienceCode: 60480101MASTER THESIS OF INFORMATION TECHNOLOGYSI'PERVISOR: Assoc. Prof. Nguyen Viet Ha Dr. -Mohamed Fa Avoiding state space explosion in model checker

ouzi AtigHanoi - 2014Declaration of AuthorshipIhereby declare that this submission is my own work and to the best of my knowledge it contains no mater

Avoiding state space explosion in model checker

ials previously published or written by another person, or sulnstanlial proportions of material which have been accepted for t he award of any ot her

VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF

Avoiding state space explosion in model checker made in the thesis. Any contribution made to the research by others, with whom 1 have worked al UET/Collech or elsewhere, is explicitly acknowledged i

n the thesis. I also declare that, the intellectual content of this t hesis is the product of my own work, except to the extent that assistance from o Avoiding state space explosion in model checker

thers in the project’s design ami conception or in style, presentation and linguistic expression is acknowledged.Signed:Date:https://khothuvien.coniAB

Avoiding state space explosion in model checker

STRACTModel-checking is a well-known technique for the program verification problem (i.e., checking t hat, the program sat isfies a given property)- H

VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF

Avoiding state space explosion in model checker eveloping new efficient, techniques to address t lie statespace explosion problem (such as slicing) is a crucial and difficult challenge in Modelcheck

ing.In t his thesis, we present a new slicing method for handling Hie standard stale explosion problem. Our slicing method consists of three steps: (I Avoiding state space explosion in model checker

) creating an abstraction wit h respect to a subset of program variables, which leads tn an over-approximation of the input program. (2) reconst metin

Avoiding state space explosion in model checker

g a program with another sul>set of variables from a counterexample of abstracted program, and (3) refining the abstraction if the counterexample is a

VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF

Avoiding state space explosion in model checker iables. In the former case, the program is correct: in the lat ter case, the program contains an error. We have implemented a prototype tool and run i

t successfully on standard benchmarks, together with several challenging examples. The experimental results show t he efficiency of our method.iiA ckn Avoiding state space explosion in model checker

0 w I edg e m e n tsFirst and foremost, 1 would like to express my deepest gratitude to my supervisor. Assoc. Prof. Nguyen Viet Ha, for his patient g

Avoiding state space explosion in model checker

uidance and continuous support throughout the yeans. I would like to give my honest appreciation to my co-supervisor Dr. Mohamed Faouzi Atig and Prof.

VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF

Avoiding state space explosion in model checker from my family, my friends in ƯET-VNƯH and Uppsala University, and my girl friend, Diu Cap, is also very important for me. When reading this thesis,

if you find any mistakes, sending to me at d iepbpXtvnu.edu. vn is appreciated.iiiContentsDeclaration of AuthorshipỈAcknowledgementsiiiContentsIvList Avoiding state space explosion in model checker

of FiguresVỈList of Tablesvii1Introduction1

VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF