Using Answer Set Programming in the Development of Verified Software

Schanda, Florian; Brain, Martin

doi:10.4230/LIPIcs.ICLP.2012.72

Document

Using Answer Set Programming in the Development of Verified Software

Authors Florian Schanda, Martin Brain

Part of: Volume: Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (ICLP 2012)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Logic Programming (ICLP)
License: Creative Commons Attribution-NoDerivs 3.0 Unported license
Publication Date: 2012-09-05

PDF

File

PDF

LIPIcs.ICLP.2012.72.pdf

Filesize: 0.83 MB
14 pages

Document Identifiers

DOI: 10.4230/LIPIcs.ICLP.2012.72
URN: urn:nbn:de:0030-drops-36114

Subject Classification

Keywords

Answer Set Programming
verification
SPARK
Ada
contract based verification
safety critical

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

Software forms a key component of many modern safety and security critical systems. One approach to achieving the required levels of assurance is to prove that the software is free from bugs and meets its specification. If a proof cannot be constructed it is important to identify the root cause as it may be a flaw in the specification or a bug. Novice users often find this process frustrating and discouraging, and it can be time-consuming for experienced users. The paper describes a commercial application based on Answer Set Programming called Riposte. It generates simple counter-examples for false and unprovable verification conditions (VCs). These help users to understand why problematic VC are false and makes the development of verified software easier and faster.

Cite As Get BibTex

Florian Schanda and Martin Brain. Using Answer Set Programming in the Development of Verified Software. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 72-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012) https://doi.org/10.4230/LIPIcs.ICLP.2012.72

Author Details

Florian Schanda

Martin Brain

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail