@mastersthesis{fpadder-cb,
  author =	{Christoph Berg},
  title =	{Formal Verification of an {IEEE} Floating Point Adder},
  school =	{Saarland University, Computer Science Department},
  month =	may,
  year =	2001,
  PSGZ =	{2001/fpadder-cb.ps.gz},
  pdf =		{2001/fpadder-cb.pdf},
  pvs =		{2001/fpadder-cb-pvsfiles.tgz},
  bibtex =	{2001/fpadder-cb.bib},
  abstract =	{Our group at Saarland University is formally verifying the correctness of a
	complete microprocessor called VAMP. The PVS theorem prover is used to specify
	the circuit definitions and to prove their correctness.
	For the VAMP project, a library of basic circuits was developed. The formal
	verification of this library is described in the first part of this thesis.
	Part of the VAMP is an IEEE compliant floating point unit. The second part of
	this thesis describes the formal verification of the gate level correctness of
	the VAMP floating point adder.},
}