Abstrakt. Booleska program, tvingande program där alla variabler har typ boolean, har använts effektivt som abstraktioner av enhetsdrivrutiner (i Ball och Rajamani SLAM projekt). För att hitta fel i dessa booleska program använder SLAM en modellkontroll baserad på binära beslutsscheman (BDD). Som en alternativ kontrollmetod definierar detta papper semantik av booleska program genom svagaste lösningar av rekursiva svagaste-förutsättningar ekvationer. Dessa ekvationer översätts sedan till ett tillfredsställande (SAT) problem. Metoden använder både BDD och SAT lösning, och det möjliggör en on-the-fly kompromiss mellan symbolisk och explicit-state representation av programmets ursprungliga tillstånd. Booleska program är tvingande datorprogram där alla variabler har typ boolean. De har visat sig vara användbara abstraktioner av lågnivåsystemprogramvara. I synnerhet har booleska program använts som abstraktioner av enhetsdrivrutiner, som används i Ball och Rajamani SLAM projekt [2]. I den här artikeln visar jag hur man översätter ett booleskt program till en logisk formel som (a) är tillfredsställande om och endast om det finns en väg från programmets början till ett fel och (b) kan användas som input till en satisfiability (SAT) lösare. Översättningen börjar med semantiken i booleska programmet, som jag definierar som den svagaste lösningen på en uppsättning svagaste-förutsättning ekvationer. Den största utmaningen är då att omvandla den andra-order fixpoint karakteriseringen till en första-order propositionell formel. Jag presenterar en algoritm för att göra det. Algoritmen bygger på tre matematiska ingredienser, vilket jag förklarar. Översättningen till en SAT formel använder binära beslut diagram (BDD) [5]. En enkel matematisk jämlikhet gör att den symboliska representationen av programmets ursprungliga värden kan ändras, i farten, till en representation som modellerar dessa booleska värden explicit. På grund av denna uttryckliga representation kan de BDD som används göras godtyckligt enkla. Tidningen går vidare enligt följande. Sekreterare 1 definierar booleska program och deras svagaste precondition semantik. Sekreterare 2 presenterar de tre matematiska ingredienser som översättningen baseras på. Sekreterare 3 sedan presenterar översättningsalgoritmen. Sekreterare 4 diskuterar komplexiteten i algoritmen, tar fram sin symboliska-versus-explicit-stat kompromisser, och rapporterar om några preliminära experiment. Papperet avslutas sedan med en del relaterat arbete och en slutsats.
Vår teorem har redan hittat en användning, nämligen i översättningen av booleska program till tillfredsställande formler REF.
A SAT Characterization of Boolean-Program Correctness
{'venue': 'SPIN', 'journal': None, 'mag_field_of_study': ['Computer Science']}