Formal verification of software source code through semi-automatic modeling |
| |
| Authors: | Cindy Eisner |
| |
| Affiliation: | (1) IBM Haifa Research Laboratory, Haifa University Campus, Mount Carmel, Haifa, 31905, Israel |
| |
| Abstract: | We describe the experience of modeling and formally verifying a software cache algorithm using the model checker RuleBase. Contrary to prevailing wisdom, we used a highly detailed model created directly from the C code itself, rather than a high-level abstract model. |
| |
| Keywords: | Software model checking Software verification Program verification Functional verification |
| 本文献已被 SpringerLink 等数据库收录！ |
|
