Title :
Comparing techniques for proving unsatisfiability
Author :
Tveretina, Olga ; Zantema, Hans
Author_Institution :
Dept. of Comput. Sci., Tech. Univ. of Eindhoven, Netherlands
Abstract :
We compare two standard techniques for satisfiability (SAT), which are basic for verification of microprocessor systems. We propose an approach for construction of shorter resolution refutations based on a standard approach called DPLL.
Keywords :
computability; digital signal processing chips; fault diagnosis; formal verification; microprocessor chips; DPLL; digital signal processor; fault diagnosis; formal verification; microprocessor system verification; propositional logic; satisfiability problem; shorter resolution refutations; software verification; standard techniques for satisfiability; unsatisfiability; Circuit faults; Computer science; Digital signal processors; Electronic design automation and methodology; Fault diagnosis; Formal verification; Hardware; Logic; Microprocessors; Signal resolution;
Conference_Titel :
Mathematical Methods in Electromagnetic Theory, 2002. MMET '02. 2002 International Conference on
Conference_Location :
Kiev, Ukraine
Print_ISBN :
0-7803-7391-X
DOI :
10.1109/MMET.2002.1107033
