Verification of Programs via Intermediate Interpretation
We explore an approach to verification of programs via program transformation applied to an interpreter of a programming language. A specialization technique known as Turchin's supercompilation is used to specialize some interpreters with respect to the program models. We show that several safe...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2017-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1708.09002v1 |
| _version_ | 1811305509023645696 |
|---|---|
| author | Alexei P. Lisitsa Andrei P. Nemytykh |
| author_facet | Alexei P. Lisitsa Andrei P. Nemytykh |
| author_sort | Alexei P. Lisitsa |
| collection | DOAJ |
| description | We explore an approach to verification of programs via program transformation applied to an interpreter of a programming language. A specialization technique known as Turchin's supercompilation is used to specialize some interpreters with respect to the program models. We show that several safety properties of functional programs modeling a class of cache coherence protocols can be proved by a supercompiler and compare the results with our earlier work on direct verification via supercompilation not using intermediate interpretation.
Our approach was in part inspired by an earlier work by E. De Angelis et al. (2014-2015) where verification via program transformation and intermediate interpretation was studied in the context of specialization of constraint logic programs. |
| first_indexed | 2024-04-13T08:26:34Z |
| format | Article |
| id | doaj.art-302946474be24426b712c5c14132233c |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T08:26:34Z |
| publishDate | 2017-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-302946474be24426b712c5c14132233c2022-12-22T02:54:24ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-08-01253Proc. VPT 2017547410.4204/EPTCS.253.6:2Verification of Programs via Intermediate InterpretationAlexei P. Lisitsa0Andrei P. Nemytykh1 Department of Computer Science, The University of Liverpool Program Systems Institute, Russian Academy of Sciences We explore an approach to verification of programs via program transformation applied to an interpreter of a programming language. A specialization technique known as Turchin's supercompilation is used to specialize some interpreters with respect to the program models. We show that several safety properties of functional programs modeling a class of cache coherence protocols can be proved by a supercompiler and compare the results with our earlier work on direct verification via supercompilation not using intermediate interpretation. Our approach was in part inspired by an earlier work by E. De Angelis et al. (2014-2015) where verification via program transformation and intermediate interpretation was studied in the context of specialization of constraint logic programs.http://arxiv.org/pdf/1708.09002v1 |
| spellingShingle | Alexei P. Lisitsa Andrei P. Nemytykh Verification of Programs via Intermediate Interpretation Electronic Proceedings in Theoretical Computer Science |
| title | Verification of Programs via Intermediate Interpretation |
| title_full | Verification of Programs via Intermediate Interpretation |
| title_fullStr | Verification of Programs via Intermediate Interpretation |
| title_full_unstemmed | Verification of Programs via Intermediate Interpretation |
| title_short | Verification of Programs via Intermediate Interpretation |
| title_sort | verification of programs via intermediate interpretation |
| url | http://arxiv.org/pdf/1708.09002v1 |
| work_keys_str_mv | AT alexeiplisitsa verificationofprogramsviaintermediateinterpretation AT andreipnemytykh verificationofprogramsviaintermediateinterpretation |