# LaTeX2HTML 96.1 (Feb 5, 1996)
# Associate contents original text with physical files.

$key = q/0 0 0 7 6 10 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node54.html%:%A complete specification file' unless ($toc_section_info{$key}); 
$key = q/0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '0%:%tut.html%:%The Bandera Tools for Model-checking Java Source Code: <BR> A User's Manual' unless ($toc_section_info{$key}); 
$key = q/0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node1.html%:%Contents' unless ($toc_section_info{$key}); 
$key = q/0 0 0 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node2.html%:%List of Figures' unless ($toc_section_info{$key}); 
$key = q/0 0 0 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node3.html%:%Introduction' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node4.html%:%Overview' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node16.html%:%Installation' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node6.html%:%When might someone be interested in learning about Bandera?' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node25.html%:%Overview of the Bandera User Interface' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node18.html%:%Installing' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node34.html%:%Guided Tour' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node55.html%:%The Bandera Specification Language' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node8.html%:%Java infrastructure and intermediate representation:' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node19.html%:%UNIX' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node27.html%:%Sessions' unless ($toc_section_info{$key}); 
$key = q/0 0 0 9 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node70.html%:%The BUI Predicate Manager' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 2 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node20.html%:%Windows <tex2html_image_mark>#tex2html_wrap_inline4316# 95/98/Me' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node23.html%:%Compiling' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node36.html%:%Windows<tex2html_image_mark>#tex2html_wrap_inline4338#' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node57.html%:%Design Rationale' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 3 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node10.html%:%Property specification:' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 2 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node21.html%:%Windows <tex2html_image_mark>#tex2html_wrap_inline4318# NT 4.0 or Windows <tex2html_image_mark>#tex2html_wrap_inline4320# 2000' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node29.html%:%Session Manager' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node38.html%:%Simple Deadlock with Slicing' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 6 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node31.html%:%The PDG Browser' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 5 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node12.html%:%Approach to model construction:' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 3 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node59.html%:%Rationale' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node62.html%:%The Temporal Specification Sublanguage' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node44.html%:%Bounded Buffer Example' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 4 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node64.html%:%Syntax and informal semantics' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 8 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node33.html%:%Pull-down Menus' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 7 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node14.html%:%Abstract interpretation:' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node45.html%:%The structure of the Bounded Buffer example' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 3 0 3 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node61.html%:%Implementation issues' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 4 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node65.html%:%Implicit Constraints' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 5 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node67.html%:%Specifying Properties for Class Instances' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node46.html%:%Bounded Buffer requirements' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node47.html%:%Requirement one' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node48.html%:%Requirement two' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node49.html%:%Requirement three' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 6 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node50.html%:%Requirement four' unless ($toc_section_info{$key}); 
$key = q/0 0 0 11 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node73.html%:%Appropriate notions of dependence for concurrent Java' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 7 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node51.html%:%Requirement five' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 8 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node52.html%:%Building a session for requirement one' unless ($toc_section_info{$key}); 
$key = q/0 0 0 11 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node75.html%:%Using the dependency browser' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 6 9 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node53.html%:%Building a session for requirement three' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node5.html%:%Challenges of model-checking program source code' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node17.html%:%Requirements' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node26.html%:%The Project and Code Panels' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node7.html%:%Architecture of Bandera' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node35.html%:%UNIX or Linux' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node22.html%:%Package Contents' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node28.html%:%Component Buttons' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 2 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node9.html%:%Java front-end:' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node56.html%:%Introduction' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node37.html%:%Simple Deadlock' unless ($toc_section_info{$key}); 
$key = q/0 0 0 5 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node24.html%:%Running and The First Launch' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node58.html%:%The Assertion Sublanguage' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 4 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node11.html%:%Static analysis:' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node30.html%:%Property Specification Buttons' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node39.html%:%Pipeline Example' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 5 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node66.html%:%Specifying Temporal Patterns' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 4 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node63.html%:%Predicate Definition Sublanguage' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 3 0 2 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node60.html%:%Syntax and informal semantics' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 6 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node13.html%:%Slicing:' unless ($toc_section_info{$key}); 
$key = q/0 0 0 6 7 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node32.html%:%Abstract Type Inference' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 5 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node40.html%:%The structure of the Pipeline example' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 5 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node68.html%:%Universal Class Instance Quantification' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 5 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node41.html%:%Writing a specification using the Bandera
Specification Language' unless ($toc_section_info{$key}); 
$key = q/0 0 0 8 5 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node69.html%:%Implementation Issues' unless ($toc_section_info{$key}); 
$key = q/0 0 0 4 3 0 8 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '6%:%node15.html%:%Back end model generation:' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 5 3 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node42.html%:%Entering a specification using the Bandera
User Interface' unless ($toc_section_info{$key}); 
$key = q/0 0 0 7 5 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '5%:%node43.html%:%Using a simple data abstraction' unless ($toc_section_info{$key}); 
$key = q/0 0 0 10 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node71.html%:%The BUI Pattern Manager' unless ($toc_section_info{$key}); 
$key = q/0 0 0 11 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node72.html%:%The Bandera Slicer' unless ($toc_section_info{$key}); 
$key = q/0 0 0 12 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node76.html%:%The Bandera Abstraction Tools' unless ($toc_section_info{$key}); 
$key = q/0 0 0 11 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '4%:%node74.html%:%How slicing criteria are generated' unless ($toc_section_info{$key}); 
$key = q/0 0 0 13 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node77.html%:%Limitations and Known Bugs' unless ($toc_section_info{$key}); 
$key = q/0 0 0 14 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node78.html%:%References' unless ($toc_section_info{$key}); 
$key = q/0 0 0 15 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0/;
$toc_section_info{$key} = '3%:%node79.html%:%  About this document ... ' unless ($toc_section_info{$key}); 

1;

