A proof repository for formal verification of software

M.G.J. Franssen

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

    82 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

    Dive into the research topics of 'A proof repository for formal verification of software'. Together they form a unique fingerprint.

    Cite this