Abstrakt. Vi presenterar ett nytt beslutsförfarande för finit-precision bitvektor aritmetik med godtycklig bit-vektor operationer. Vårt förfarande växlar mellan att generera under- och över-uppskattningar av den ursprungliga bit-vektor formel. En under- approximation erhålls genom en översättning till propositionslogik där vissa bit-vektor variabler kodas med färre booleska variabler än deras bredd. Om under- approximationen inte är tillfredsställande, använder vi den otillfredsställande kärnan för att härleda en över- approximation baserad på den delmängd av predikat som deltog i beviset på otillfredsställande. Om denna över- approximation är tillfredsställande, den tillfredsställande uppgiften styr förfiningen av den tidigare under approximationen genom att, för några bit-vektor variabler, öka antalet booleska variabler som kodar dem. Vi presenterar experimentella resultat som tyder på att denna abstraktion baserad metod kan vara betydligt effektivare än att direkt åberopa SAT-lösaren på den ursprungliga formeln samt andra konkurrerande beslutsförfaranden.
nyligen föreslagna abstraktion baserade beslutsförfaranden för bit-vektor aritmetisk REF.
Deciding bit-vector arithmetic with abstraction
{'venue': 'IN PROC. TACAS 2007', 'journal': None, 'mag_field_of_study': ['Computer Science']}