A proof repository for formal verification of software

M.G.J. Franssen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

47 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010)
EditorsH. Kienle
Pages76-94
Publication statusPublished - 2010

Fingerprint

Theorem proving
Computer programming languages
Formal verification

Cite this

Franssen, M. G. J. (2010). A proof repository for formal verification of software. In H. Kienle (Ed.), Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010) (pp. 76-94)
Franssen, M.G.J. / A proof repository for formal verification of software. Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010). editor / H. Kienle. 2010. pp. 76-94
@inproceedings{7102d4d3c8214a149f209f5523f42985,
title = "A proof repository for formal verification of software",
abstract = "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.",
author = "M.G.J. Franssen",
year = "2010",
language = "English",
pages = "76--94",
editor = "H. Kienle",
booktitle = "Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010)",

}

Franssen, MGJ 2010, A proof repository for formal verification of software. in H Kienle (ed.), 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.

Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010). ed. / H. Kienle. 2010. p. 76-94.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 -

Franssen MGJ. A proof repository for formal verification of software. In Kienle H, editor, Proceedings of the 3rd International Workshop on Academic Software Development Tools and Techniques (WASDeTT 2010, Antwerp, Belgium, September 20, 2010). 2010. p. 76-94