DROPS

Document

DOI: 10.4230/LIPIcs.ICLP.2012.72

Using Answer Set Programming in the Development of Verified Software

Authors: Florian Schanda and Martin Brain

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

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

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)

Copy BibTex To Clipboard

@InProceedings{schanda_et_al:LIPIcs.ICLP.2012.72,
  author =	{Schanda, Florian and Brain, Martin},
  title =	{{Using Answer Set Programming in the Development of Verified Software}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{72--85},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.72},
  URN =		{urn:nbn:de:0030-drops-36114},
  doi =		{10.4230/LIPIcs.ICLP.2012.72},
  annote =	{Keywords: Answer Set Programming, verification, SPARK, Ada, contract based verification, safety critical}
}

Search Results

Documents authored by Brain, Martin

Using Answer Set Programming in the Development of Verified Software

Abstract

Cite as

Thanks for your feedback!

Could not send message