2026-07-20T12:09:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3611 2024-03-06T10:34:25Z ddc:004 open_access

Using Answer Set Programming in the Development of Verified Software Schanda, Florian Brain, Martin Answer Set Programming verification SPARK Ada contract based verification safety critical 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Florian Schanda and Martin Brain 2012 Is Part Of LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICLP.2012.72 urn:nbn:de:0030-drops-36114 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.72 eng https://creativecommons.org/licenses/by-nd/3.0/legalcode