Abstrakt. HSF(C) är ett verktyg som automatiserar verifiering av säkerhets- och livegenskaper för C-program. I detta dokument beskrivs den verifieringsmetod som används av HSF(C) och ges instruktioner om hur verktyget ska installeras och användas. HSF(C) är ett verktyg för verifiering av C-program baserat på predikativ abstraktion och förfining enligt det kontraexempelstyrda paradigmet för förfining av abstraktion (CE-GAR) [4]. Det finns ett antal framgångsrika verktyg [1, 7, 5, 10, 2] baserade på abstraktion förfining. Vi ger här en kort beskrivning av vår verifieringsalgoritm; intresserade läsare kan hitta mer information om den underliggande teorin bakom vårt genomförande i [10, 6]. Algoritmen som används i HSF(C) är en generalisering av CEGAR-systemet som behandlar Hornliknande klausuler istället för övergångssystem/program med procedurer. Vi använder Hornklausuler för att representera både det program som ska verifieras och den bevisregel som används för verifiering, dvs. säkerhetskontroll för program med procedurer. Bevisregeln listar lokaler för programsäkerhet och kräver kompletterande påståenden som representerar induktiva invarianter. Med Hornklausuler som ingång, fortsätter vår algoritm i tre steg. 1. Vad är det för fel på dig? Med en fast uppsättning predikat, initialt tomma, hittar vi en lösning för de kompletterande påståendena. Vid detta steg utför vi logiska slutsatser och förlitar oss på abstraktion för att säkerställa uppsägning i närvaro av rekursion och för att säkerställa effektivitet i närvaro av stora uppsättningar av klausuler. 2. Utgångspunkten är följande: Vi kontrollerar om den beräknade lösningen uppfyller programsäkerheten. I så fall lyckas verifieringen och algoritmen returnerar "säker". 3. Vad är det som händer? Vi kontrollerar om den logiska slutsatsen som görs i det första steget i inställningen utan någon abstraktion ger en lösning som fortfarande bryter mot programsäkerheten. Om överträdelsen fortfarande är närvarande så returnerar vi "osäkra" och inferenceträdet som en felväg som når felplatsen. Annars använder vi den erhållna lösningen för att förfina abstraktionsfunktionen och gå tillbaka till det första steget.
Ett antal verktyg för genomförande av predikativ abstraktion och förfining finns tillgängliga, t.ex. HSF REF och BLAST [2].
HSF(C): A Software Verifier Based on Horn Clauses (Competition Contribution)
{'venue': 'TACAS', 'journal': None, 'mag_field_of_study': ['Computer Science']}