In this paper, we apply lightweight formal methods to address the 
problem of vulnerabilities in software applications.  Our approach 
bridges the gap between formal methods verification and security 
problems because most security constraints can be formulated as an 
integer range constraint problem.  We leverage an existing tool set 
and an automated verifier to provide a solution to the buffer overflow 
vulnerability problem that is both precise and scalable.  We describe 
an implementation of our approach that has proven successful in the 
test cases that  we consider.  In the next section, we provide an 
overview of our approach.  In the full paper, we provide a complete 
description of the methodology and the results of our case study.