TY  - CONF
AU  - Tronci, Enrico
PY  - 1995
DA  - 1995//
TI  - Hardware Verification, Boolean Logic Programming, Boolean Functional Programming
BT  - Tenth Annual IEEE Symposium on Logic in Computer Science (LICS)
SP  - 408
EP  - 418
PB  - IEEE Computer Society
CY  - San Diego, California
AB  - One of the main obstacles to automatic verification of finite state systems (FSSs) is state explosion. In this respect automatic verification of an FSS M using model checking and binary decision diagrams (BDDs) has an intrinsic limitation: no automatic global optimization of the verification task is possible until a BDD representation for M is generated. This is because systems and specifications are defined using different languages. To perform global optimization before generating a BDD representation for M we propose to use the same language to define systems and specifications. We show that first order logic on a Boolean domain yields an efficient functional programming language that can be used to represent, specify and automatically verify FSSs, e.g. on a SUN Sparc Station 2 we were able to automatically verify a 64 bit commercial multiplier.
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Tronci1995.pdf
UR  - https://doi.org/10.1109/LICS.1995.523275
DO  - 10.1109/LICS.1995.523275
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=56), last updated on Sat, 24 Nov 2012 14:34:24 +0100
ID  - Tronci1995
ER  -