@InProceedings{bjk01:basics,
  title =	{Formal Verification of a Basic Circuits Library},
  author =	{Christoph Berg and Christian Jacobi and Daniel Kroening},
  journal =	{Proc.\ of the IASTED International Conference on Applied Informatics, Innsbruck (AI 2001)},
  booktitle =	{Applied Informatics 2001},
  pages =	{252--255},
  month =	feb,
  year =	{2001},
  publisher =	{ACTA Press},
  ps =		{2001/basiccircuits.ps},
  psgz =	{2001/basiccircuits.ps.gz},
  pdf =		{2001/basiccircuits.pdf},
  slides =	{2001/basiccircuits-slides.ps.gz},
  bibtex =	{2001/basiccircuits.bib},
  abstract =	{We describe the results and status of a project aiming to provide a provably
	correct library of basic circuits. We use the theorem proving system PVS
	in order to prove circuits such as incrementers, adders, arithmetic units,
	multipliers, leading zero counters, shifters, and decoders.
	All specifications and proofs are available on the web.}
}