Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01
➤ Gửi thông báo lỗi ⚠️ Báo cáo tài liệu vi phạmNội dung chi tiết: Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01
Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01
VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 INFORMATION TECHNOLOGYHanoi - 2014VIETNAM NATIONAL UNIVERSITY, HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBIT PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMajor: Computer scienceCode: 60480101MASTER THESIS OF INFORMATION TECHNOLOGYSI'PERVISOR: Assoc. Prof. Nguyen Viet Ha Dr. -Mohamed Fa Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 ouzi AtigHanoi - 2014Declaration of AuthorshipIhereby declare that this submission is my own work and to the best of my knowledge it contains no materLuận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01
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 Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 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 in 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 Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 thers in the project’s design ami conception or in style, presentation and linguistic expression is acknowledged.Signed:Date:https://khothuvien.coniABLuận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01
STRACTModel-checking is a well-known technique for the program verification problem (i.e., checking t hat, the program sat isfies a given property)- HVIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 eveloping new efficient, techniques to address t lie statespace explosion problem (such as slicing) is a crucial and difficult challenge in Modelchecking.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 Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 ) creating an abstraction wit h respect to a subset of program variables, which leads tn an over-approximation of the input program. (2) reconst metinLuận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01
g a program with another sul>set of variables from a counterexample of abstracted program, and (3) refining the abstraction if the counterexample is aVIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 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 it successfully on standard benchmarks, together with several challenging examples. The experimental results show t he efficiency of our method.iiA ckn Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 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 gLuận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01
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 Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 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 Luận văn thạc sĩ VNU UET avoiding state space explosion in model checker m a thesis information technology 60 48 01 of FiguresVỈList of Tablesvii1Introduction1VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OF VIETNAM NATIONAL UNIVERSITY. HANOIUNIVERSITY OF ENGINEERING AND TECHNOLOGYBUI PHI DIEPAVOIDING STATE-SPACE EXPLOSION IN MODEL-CHECKERMASTER THESIS OFGọi ngay
Chat zalo
Facebook