Tata Institute of Fundamental Research
Proof Transformations for Verification
Seminar
Speaker:
Ashutosh K. Gupta (Institute of Science and Technology, Austria
Am Campus 1
3400 Klosterneuburg
Austria)
Date:
Friday, 12 Oct 2012, 15:30 to 16:30
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
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: | Ashutosh K. Gupta (Institute of Science and Technology, Austria Am Campus 1 3400 Klosterneuburg Austria) |
| Date: | Friday, 12 Oct 2012, 15:30 to 16:30 |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
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.
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.