5
$\begingroup$

I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there any other frameworks for proving program equivalence?

$\endgroup$
  • $\begingroup$ This is a pretty general question: in general program verification is domain specific: you're trying to verify something in particular, e.g. safety or security, or the programs themselves are in a very constrained language. Do you have use-cases in mind? Are you trying to verify full functional equivalence? Something even stronger? $\endgroup$ – cody May 13 at 13:15
0
$\begingroup$

One general approach to the problem is to prove program equivalence by showing the programs have the same semantics. Hoare-style verification, as you say, is one option categorized as axiomatic semantics. Have a look at this article which describes most of the semantic approaches out there, including denotational semantics and operational semantics.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.