Formal approach to program verification

Chatchai Koetsawat

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/2844

Full metadata record

DC Field	Value	Language
dc.contributor.advisor	Peraphon Sophatsathit	-
dc.contributor.author	Chatchai Koetsawat	-
dc.contributor.other	Chulalongkorn University. Faculty of Science	-
dc.date.accessioned	2006-09-26T06:33:45Z	-
dc.date.available	2006-09-26T06:33:45Z	-
dc.date.issued	2001	-
dc.identifier.isbn	9741702795	-
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/2844	-
dc.description	Thesis (M.Sc.)--Chulalongkorn University, 2001	en
dc.description.abstract	Program verification has played an important role in today's production of reliable software [3]. The most popular method of verification is given by Hoare. Other mathematicians and programmers also offered their method based on Hoare's principles. This thesis proposes a different approach to program verification using Hoare notation. In this thesis, we introduced a new method based on Hoare triple and some inference rules as a tool for program correctness proof. The proposed approach adopted conventional black-box and white-box tests [6] to carried out a systematic and rigorous program verification.	en
dc.description.abstractalternative	ในกระบวนการผลิตซอฟแวร์ที่มีความน่าเชื่อถือนั้น การตรวจสอบความถูกต้องของโปรแกรมมีความสำคัญมาก ซึ่งวิธีการตรวจสอบที่เป็นรู้จักกันดีได้แก่ วิธีที่นำเสนอโดย Hoare และหลังจากนั้นได้มีนักคณิตศาสตร์และ โปรแกรมเมอร์จำนวนมากที่อาศัยพื้นฐานจากวิธีการของ Hoare ในการสร้างวิธีการตรวจสอบใหม่ๆ รวมถึงงานวิจัยชิ้นนี้ด้วย ในงานวิจัยชิ้นนี้ได้นำเสนอวิธีการตรวจสอบความถูกต้องของโปรแกรม โดยใช้ Hoare triple และ Rule of Inference เป็นพื้นฐานในการสร้างวิธีการตรวจสอบความถูกต้องของโปรแกรม เนื่องจากมีการประยุกต์การตรวจสอบแบบ Black-Box และ White-Box อย่างมีระบบแน่นอน มาใช้ในกระบวนการนี้ด้วย	-
dc.format.extent	3413471 bytes	-
dc.format.mimetype	application/pdf	-
dc.language.iso	en	en
dc.publisher	Chulalongkorn University	en
dc.rights	Chulalongkorn University	en
dc.subject	Computer programs--Verification	en
dc.subject	Computer software--Verification	en
dc.title	Formal approach to program verification	en
dc.title.alternative	วิธีการตรวจสอบโปรแกรมโดยหลักการเชิงรูปนัย	en
dc.type	Thesis	en
dc.degree.name	Master of Science	en
dc.degree.level	Master's Degree	en
dc.degree.discipline	Computational Science	en
dc.degree.grantor	Chulalongkorn University	en
dc.email.advisor	peraphon.s@chula.ac.th	-
Appears in Collections:	Sci - Theses

Files in This Item:

File	Description	Size	Format
Chatchai.pdf		1.47 MB	Adobe PDF	View/Open

Show simple item record