Transforming Programs into Recursive Functions
| Autor: | Magnus O. Myreen, Michael J. C. Gordon |
|---|---|
| Rok vydání: | 2009 |
| Předmět: |
Theoretical computer science
General Computer Science Function (mathematics) Separation logic Hoare logic Theoretical Computer Science program verification Automated theorem proving Computer-assisted proof theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Recursive functions Calculus Computer Science(all) Mathematics |
| Zdroj: | Electronic Notes in Theoretical Computer Science. 240:185-200 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2009.05.052 |
| Popis: | This paper presents a new proof-assistant based approach to program verification: programs are translated, via fully-automatic deduction, into tail-recursive function defined in the logic of a theorem prover. This approach improves on well-established methods based on Hoare logic and verification condition generation (VCG) by removing the need to annotate programs with assertions, making the proof natural to the theorem prover and being easier to implement than a trusted VCG. Our tool has been implemented in the HOL4 theorem prover. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect