@STRING{ lncs="Lecture notes in computer science" }

@BOOK{ Knuth:TeX,
  author="Knuth, Donald E.",
  title="The {\TeX} book",
  publisher="Addison-Wesley",
  year=1984
}

@BOOK{ Lamport:LaTeX,
  author="Lamport, Leslie",
  title="{\LaTeX}: A Document Preparation System (2nd Edition)",
  publisher="Addison-Wesley",
  year=1994,
  note="See also \cite{Knuth:TeX}."
}

@INBOOK{ Grandstrand,
  author = {O. Grandstrand},
  title = {Innovation and Intellectual Property Rights},
  chapter = 2,
  crossref = {Fberg04}
}

@BOOK{ Fberg04,
  editor = {J. Fagerberg and D.C. Mowery and R.R. Nelson}, 
  title = {Oxford Handbook of Innovation},
  booktitle = {Oxford Handbook of Innovation},
  publisher = {Oxford University Press},
  address = {Oxford, UK},
  volume=1,
  year = 2004
}

@book{Goo93,
  author    = "Goossens, Michel and Mittelbach, Frank and Samarin, Alexander",
  title     = "The {\LaTeX} Companion",
  year      = "1993",
  publisher = "Addison-Wesley",
  address   = "Reading, Massachusetts"
}

@inproceedings{deMouraBjorner:Z3:overview,
  author    = "de Moura, Leonardo and Nikolaj Bj{\o}rner",
  title     = {{Z3}: An efficient {SMT} solver},
  booktitle = {Tools and Algorithms for the Construction and
                  Analysis of Systems, 14th International Conference,
                  TACAS 2008},
  editor    = {C. R. Ramakrishnan and Jakob Rehof},
  series    = lncs,
  volume    = 4963,
  publisher = {Springer},
  month     = mar # "--" # apr,
  year      = 2008,
  pages     = {337-340},
}

@InProceedings{Lean:CADE2015,
  author =       {de Moura, Leonardo and Soonho Kong and Jeremy Avigad and
                  van Doorn, Floris and von Raumer, Jakob},
  title =        {The {L}ean Theorem Prover (System Description)},
  booktitle =    {Automated Deduction --- CADE-25 --- 25th International
                  Conference on Automated Deduction},
  editor =       {Amy P. Felty and Aart Middeldorp},
  series =       lncs,
  volume =       {9195},
  year =         {2015},
  pages =        {378-388},
  month =        aug,
  publisher =    {Springer},
}
