Removing Unnecessary Variables from Horn Clause Verification Conditions

Removing Unnecessary Variables from Horn Clause Verification Conditions

Verification conditions (VCs) are logical formulas whose satisfiability guarantees program correctness. We consider VCs in the form of constrained Horn clauses (CHC) which are automatically generated from the encoding of (an interpreter of) the operational semantics of the programming language. VC...

Full description

Bibliographic Details
Main Authors: Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
Format: Article
Language:English
Published: Open Publishing Association 2016-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1607.04460v1

Internet

http://arxiv.org/pdf/1607.04460v1

Similar Items