Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
The proof of a program property can be reduced to the proof of satisfiability of a set of constrained Horn clauses (CHCs) which can be automatically generated from the program and the property. In this paper we have conducted a case study in Horn clause verification by considering several sorting p...
Main Authors: | , , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2019-07-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1907.03999v1 |