Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/35815
Title: Efficiently verifying programs with rich control flows
Authors: GHERGHINA CRISTIAN ANDREI
Keywords: verification exceptions barriers specialization logic flow
Issue Date: 23-Aug-2012
Source: GHERGHINA CRISTIAN ANDREI (2012-08-23). Efficiently verifying programs with rich control flows. ScholarBank@NUS Repository.
Abstract: We introduce a sound verification logic that efficiently handles multithreaded programs with complex control flow patterns. We define an extension of separation logic that uniformly handles exceptions, program errors and other types of sequential control flows through the use of a uniform formalism for expressing both static and dynamic control flows. A second component handles Pthreads barriers. Barriers enable simultaneous resource ownership redistribution between multiple threads and are inherently stateful, leading to significant complications in the design of the logic. Through the use of a specialized form of inductive predicates, we equip our logic with a novel mechanism for explicitly capturing and reasoning about barrier behavior. The last essential component introduces a novel predicate specialization that reduces the performance penalty induced by user-defined disjunctive predicates by symbolically pruning infeasible disjuncts inside each predicate instance. Experimental results shown predicate specialization induced speed-ups of up to 10 fold when discharging proof obligations generated by the verification of general sequential programs and up to 37 fold for barrier reasoning.
URI: http://scholarbank.nus.edu.sg/handle/10635/35815
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
GherghinaCA.pdf1.95 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

231
checked on Dec 11, 2017

Download(s)

268
checked on Dec 11, 2017

Google ScholarTM

Check


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