f the program. It consists of:
  <ul>
    <li><tt>Environment</tt> - a mapping from source code expressions to symbolic 
    values
    <li><tt>Store</tt> - a mapping from memory locations to symbolic values
    <li><tt>GenericDataMap</tt> - constraints on symbolic values
  </ul>
  
  <h3 id=interaction>Interaction with Checkers</h3>

  <p>
  Checkers are not merely passive receivers of the analyzer core changes - they 
  actively participate in the <tt>ProgramState</tt> construction through the
  <tt>Gener