@inproceedings{23e35b4f157445b1bfad0b3b1fa6df70,
title = "Automatic generation of invariants in processor verification",
abstract = "A central task in formal verification is the definition of invariants, which characterize the reachable states of the system. When a system is finites state, invariants can be discovered automatically. Our experience in verifying microprocessors using symbolic logic is that finding adequate invariants is extremely time-consuming. We present three techniques for automating the discovery of some of these invariants. All of them are essentially syntactic transformations on a logical formula derived from the state transition function. The goal is to eliminate quantifiers and extract small clauses implied by the larger formula. We have implemented the method and exercised it on a description of the FLASH Protocol Processor (PP), a microprocessor designed at Stanford for handling communications in a multiprocessor. We had previously verified the PP by manually deriving invariants. Although the method is simple, it discovered 6 out of 7 of the invariants needed for verification of the CPU of the processor design, and 28 out of 72 invariants needed for verification of the memory system of the processor. We believe that, in the future, the discovery of invariants can be largely automated by a combination of different methods, including this one.",
author = "Su, {Jeffrey X.} and Dill, {David L.} and Barrett, {Clark W.}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1996.; 1st International Conference on Formal Methods in Computer-Aided Design, FMCAD 1996 ; Conference date: 06-11-1996 Through 08-11-1996",
year = "1996",
doi = "10.1007/BFb0031822",
language = "English (US)",
isbn = "3540619372",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "377--388",
editor = "Albert Camilleri and Mandayam Srivas",
booktitle = "Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings",
}