Abstrakt. Predicate abstraction är ett kraftfullt verktyg för att verifiera egenskaper hos infinit-state system med hjälp av en kombination av ett beslutsförfarande för en delmängd av första ordningen logik och symboliska metoder som ursprungligen utvecklats för finit-state modellkontroll. Vi betraktar modeller där systemtillståndet innehåller muterbara funktioner och predikattillståndsvariabler. En sådan modell kan beskriva system som innehåller godtyckligt stora minnen, buffertar och grupper av identiska processer. Vi beskriver en form av predikativ abstraktion som konstruerar en formel över en uppsättning universellt kvantifierade variabler för att beskriva invarianta egenskaper hos funktionstillståndsvariablerna. Vi ger en formell motivering av sundheten i vårt tillvägagångssätt och beskriver hur det har använts för att verifiera flera maskinvaru- och programvarudesigner, inklusive ett katalogbaserat cachekonsekvensprotokoll med obundna FIFO-kanaler.
Lahiri och Bryant föreslog en utvidgning av predikativ abstraktion till att sluta sig till universellt kvantifierade invarianter REF.
Constructing Quantified Invariants via Predicate Abstraction
{'venue': 'VMCAI', 'journal': None, 'mag_field_of_study': ['Computer Science']}