| Autor: |
Schanda, Florian, Brain, Martin |
| Jazyk: |
angličtina |
| Rok vydání: |
2012 |
| Předmět: |
|
| DOI: |
10.4230/lipics.iclp.2012.72 |
| Popis: |
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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
