This package consists of a set of tools targeted at finding bugs in concurrent programs written in the Boogie input language. Context-Bounded-Analysis Package (CBAP) is based on static analysis; it attempts to find bugs without executing the program. CBAP performs a bounded exploration of the set of behaviors of the concurrent program. In particular, it only explores those behaviors where the number of context switches is bounded by a given constant. Under such a bound, CBAP is able to explore a large set of concurrent behaviors efficiently.