### Abstract

Original language | English |
---|---|

Title of host publication | Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010) |

Editors | H. Kienle |

Pages | 76-94 |

Publication status | Published - 2010 |

### Fingerprint

### Cite this

*Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010)*(pp. 76-94)

}

*Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010).*pp. 76-94.

**A proof repository for formal verification of software.** / Franssen, M.G.J.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A proof repository for formal verification of software

AU - Franssen, M.G.J.

PY - 2010

Y1 - 2010

N2 - We present a proof repository that provides a uniform theorem proving interface to virtually any first-order theorem prover. Instead of taking the greatest common divisor of features supported by the first-order theorem provers, the design allows us to support any extension of the logic that can be expressed in first-order logic. If a theorem prover has native support for such a logic, this is exploited. If the prover has no such support, the repository automatically uses the first-order encoding of the extension. A built-in proof assistant is provided that allows the user to manually guide the proving process when all provers fail to prove a theorem. To prove sub-theorems, the proof assistant is able to use the repository’s full capabilities. The repository also maintains a database of proven theorems. When a requested theorem has been proved before, the result from the database is re-used instead of reconstructing the proof all over again. To test the repository, we constructed a tool for static verification of a basic programming language. This language is also described in this paper.

AB - We present a proof repository that provides a uniform theorem proving interface to virtually any first-order theorem prover. Instead of taking the greatest common divisor of features supported by the first-order theorem provers, the design allows us to support any extension of the logic that can be expressed in first-order logic. If a theorem prover has native support for such a logic, this is exploited. If the prover has no such support, the repository automatically uses the first-order encoding of the extension. A built-in proof assistant is provided that allows the user to manually guide the proving process when all provers fail to prove a theorem. To prove sub-theorems, the proof assistant is able to use the repository’s full capabilities. The repository also maintains a database of proven theorems. When a requested theorem has been proved before, the result from the database is re-used instead of reconstructing the proof all over again. To test the repository, we constructed a tool for static verification of a basic programming language. This language is also described in this paper.

M3 - Conference contribution

SP - 76

EP - 94

BT - Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010)

A2 - Kienle, H.

ER -