10.4230/LIPICS.ICLP.2012.72
Schanda, Florian
Florian
Schanda
Brain, Martin
Martin
Brain
Using Answer Set Programming in the Development of Verified Software
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2012
Article
Answer Set Programming
verification
SPARK
Ada
contract based verification
safety critical
Dovier, Agostino
Agostino
Dovier
Costa, Vítor Santos
Vítor Santos
Costa
2012
2012-09-05
2012-09-05
2012-09-05
en
urn:nbn:de:0030-drops-36114
10.4230/LIPIcs.ICLP.2012
978-3-939897-43-9
1868-8969
10.4230/LIPIcs.ICLP.2012
LIPIcs, Volume 17, ICLP 2012
Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)
2013
17
8
72
85
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dovier, Agostino
Agostino
Dovier
Costa, Vítor Santos
Vítor Santos
Costa
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2012
17
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
14 pages
880654 bytes
application/pdf
Creative Commons Attribution-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12), pages 72-85