Please use this identifier to cite or link to this item:
Title: Efficiently verifying programs with rich control flows
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.
Appears in Collections:Ph.D Theses (Open)

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



Page view(s)

checked on Dec 11, 2017


checked on Dec 11, 2017

Google ScholarTM


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