@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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.},
}