In the first part the thesis gives a short introduction to the basic concepts and mechanisms of alias analysis. The second part describes the design and implementation of AAL, the Alias Analysis Library, which is then tested experimentally. In the last section, AAL and a AAProver, a bit-precise theorem prover based on MiniSAT, is used to implement AACalysto, a static checker for arbitrary assertions in C. The whole thesis is available for download.