Please use this identifier to cite or link to this item: https://scholarbank.nus.edu.sg/handle/10635/13161
DC FieldValue
dc.titleA framework for program reasoning based on constraint traces
dc.contributor.authorANDREW EDWARD SANTOSA
dc.date.accessioned2010-04-08T10:30:33Z
dc.date.available2010-04-08T10:30:33Z
dc.date.issued2008-05-23
dc.identifier.citationANDREW EDWARD SANTOSA (2008-05-23). A framework for program reasoning based on constraint traces. ScholarBank@NUS Repository.
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/13161
dc.description.abstractWe propose a CLP-based framework that accommodates both program analysis and program verification approaches. Our framework is centered on a general verification condition computation algorithm which performs abstraction selectively. This allows for compositionality and simpler yet accurate abstraction than abstract interpretation. The algorithm is optimized between the abstraction points using a proof summarization technique. The formal foundations include modeling of programs and high-level specifications in CLP, assertions to specify traditional safety which includes recursive data structure properties, as well as structural properties (e.g., symmetry), and a proof method and techniques for proving the assertions. Our framework handles traditional safety proof, data structure verification which precision is helped by selective abstraction, and reductions using symmetry or other structural properties which can handle more cases than existing approaches. We discuss implementations of variants of our general algorithm in CLP(R) and provide their running results.
dc.language.isoen
dc.subjectprogram verification, program analysis, symbolic execution, abstraction, symmetry reduction, constraint logic programming
dc.typeThesis
dc.contributor.departmentCOMPUTER SCIENCE
dc.contributor.supervisorJAFFAR, JOXAN
dc.description.degreePh.D
dc.description.degreeconferredDOCTOR OF PHILOSOPHY
dc.identifier.isiutNOT_IN_WOS
Appears in Collections:Ph.D Theses (Open)

Show simple item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
thesis_santosa_hd993028j.pdf1.36 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

288
checked on May 22, 2019

Download(s)

247
checked on May 22, 2019

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.