Talks & Seminars
Title: Proof Transformations for Verification
Dr. Ashutosh Gupta, IST Austria
Date & Time: October 11, 2012 15:30
Venue: Conference Room, 01st Floor, C Block, Dept. of Computer Science & Engg., Kanwal Rekhi Building
Various verification methods depend on theorem provers to obtain proofs of verification conditions. If the provers return proofs that satisfy certain structure then it may enhance the performance of the verification methods. Theorem provers aim to find the proofs using the most efficient algorithms. Therefore, the returned proofs from the existing theorem provers may not satisfy such structures. In my talk, I will present two pieces of our work that transform the proofs produced by the provers to obtain such structured proofs. In the first work, we present a new efficient parametrized method to remove redundant parts of resolution proofs. The parameter allows one to choose between coverage of the redundancy removal and the efficiency of the method. In the second work, we present a set of proof transformation rules that obtains "localize proofs" from proofs of unsatisfiable formulas. The localize proofs allow one to compute (tree)-interpolants efficiently.
Speaker Profile:
Ashutosh Gupta received his Ph.D. in computer science from TUM in 2011. His Ph.D. adviser was Andrey Rybalchenko. Currently, he is a post-doctoral researcher in Henzinger group at IST Austria.
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback