Cindy Eisner, Dana Fisman, et al.
ACM TOCL
Paper
Formal verification of software source code through semi-automatic modeling
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. © Springer-Verlag 2004.
Related
Conference paper
Accurate malware detection by extreme abstraction
Fady Copty, Cindy Eisner, et al.
ACSAC 2018
Cindy Eisner, Amir Nahir, et al.
Formal Methods in System Design
Ilan Beer, Shoham Ben-David, et al.
Formal Methods in System Design