Please use this identifier to cite or link to this item:
https://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 | Citation: | 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 | Size | Format | Access Settings | Version | |
---|---|---|---|---|---|---|
GherghinaCA.pdf | 1.95 MB | Adobe PDF | OPEN | None | View/Download |
Google ScholarTM
Check
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.