@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@InProceedings{sturton-memocode13,
author = {Cynthia Sturton and Rohit Sinha and Thurston H.Y. Dang and Sakshi Jain and Michael McCoyd and Wei-Yang Tan and Petros Maniatis and Sanjit A. Seshia and David Wagner},
title = {Symbolic Software Model Validation},
booktitle = {Proceedings of the 10th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)},
month = {October},
year = {2013},
note = {To appear},
abstract = {Modeling is the crucial first step in formal verification.
Some models are constructed by humans from source
code, while others are extracted automatically by tools. Regardless of how a model is constructed, verification is only
as good as the model; therefore, it is essential to validate the
model against the implementation it represents. In this paper
we present two complementary approaches to software model
validation. The first, data-centric model validation, checks that,
for data structures relevant to the property being verified, all
operations that update these data structures are captured in the
model. The second, operation-centric model validation, checks
that each operation being modeled is correctly simulated by the
model. Both techniques are based on a combination of symbolic
execution and satisfiability modulo theories (SMT) solving. We
demonstrate the application of our methods on several case
studies, including the address translation logic in the Bochs
x86 emulator, the Berkeley Packet Filter, a TCAS benchmark
suite, the FTP server from GNU Inetutils, and a component of
the XMHF hypervisor.},
}