Skip to Main content Skip to Navigation
Conference papers

Programming Language Aggregation with Applications in Equivalence Checking

Abstract : We show that, given the operational semantics of two programming languages L and R, it is possible to construct an aggregate language, in which programs consist of pairs of programs from L and respectively R. In the aggregate language, a program P = (PL, PR) takes a step from either PL or PR. The main difficulty is how to aggregate the two languages so that data such as integers or booleans that are common to both languages has the same representation in the aggregate language. The aggregation is based on the pushout theorem, which allows us to construct a model of the aggregate language from models of the initial languages, while making sure that the interpretation of common data such as integers is the same. A main application of the aggregation result is in equivalence checking. It is possible to check for example that two programs PL and PR (written in L and respectively R) compute the same result by checking the partial correctness of the pair (PL,PR) in the aggregate language.
Document type :
Conference papers
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/hal-00998930
Contributor : Mister Dart <>
Submitted on : Tuesday, June 3, 2014 - 8:59:23 AM
Last modification on : Thursday, August 1, 2019 - 2:12:06 PM
Long-term archiving on: : Wednesday, September 3, 2014 - 11:00:37 AM

File

pas2014_submission_14_1_.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00998930, version 1

Collections

Citation

Ştefan Ciobâcǎ, Dorel Lucanu, Vlad Rusu, Grigore Rosu. Programming Language Aggregation with Applications in Equivalence Checking. Third International Seminar on Program Verification, Automated Debugging and Symbolic Computation (PAS 2014), Jul 2014, Vienne, Austria. ⟨hal-00998930⟩

Share

Metrics

Record views

287

Files downloads

413