Jasmin Christian Blanchette

Since 2008, I am a member of the Theorem Proving Group lead by Tobias Nipkow at the Technische Universität München. My research focuses on the automatic generation of counterexamples for higher-order logic using a first-order model finder. My tool Nitpick is available for download. I am financed by the project Quis Custodiet (DFG Ni 491/11-1) and affiliated to Programm- und Modell-Analyse. From 2000 to 2008, I worked as software engineer and documentation manager for Trolltech (now Qt Development Frameworks) in Oslo, Norway.

Journal Article

  • Proof pearl: Mechanizing the textbook proof of Huffman's algorithm in Isabelle/HOL
    Jasmin Christian Blanchette. Journal of Automated Reasoning 43(1), pp. 1–18, June 2009.
    Web page ⋅ PDF

Refereed Papers

  • Nitpick: A counterexample generator for higher-order logic based on a relational model finder (extended abstract)
    Jasmin Christian Blanchette and Tobias Nipkow. Third International Conference on Tests and Proofs (TAP 2009). In Dubois, C. (ed.) TAP 2009: Short Papers, ETH Technical Report 630, July 2009.
    PDF
  • Intra-object versus inter-object: Concurrency and reasoning in Creol
    Einar Broch Johnsen, Jasmin Christian Blanchette, Marcel Kyas, and Olaf Owe. 2nd International Workshop on Harnessing Theories for Tool Support in Software (TTSS 2008). To appear in Electronic Notes in Theoretical Computer Science.
    PDF
  • An open system operational semantics for an object-oriented and component-based language
    Jasmin Christian Blanchette and Olaf Owe. Electronic Notes in Theoretical Computer Science 215 (Proceedings of the 4th International Workshop on Formal Aspects of Component Software, FACS 2007), pp. 151–169, June 2008.
    Web page ⋅ PDF

Books

  • C++ GUI Programming with Qt 4 (Second Edition)
    Jasmin Blanchette and Mark Summerfield. Prentice Hall Open Source Software Development Series, Prentice Hall, February 2008.
    Chinese (Simplified), German, Korean, and Russian translations are available.
    Web page
  • C++ GUI Programming with Qt 4
    Jasmin Blanchette and Mark Summerfield. Prentice Hall, July 2006.
    Chinese (Simplified), French, German, Japanese, and Russian translations are available.
    Web page ⋅ PDF
  • C++ GUI Programming with Qt 3
    Jasmin Blanchette and Mark Summerfield. Bruce Perens' Open Source Series, Prentice Hall, January 2004.
    Chinese (Simplified), German, Japanese, and Russian translations are available.
    Web page ⋅ PDF

Other Publications

  • Monotonicity Inference for Higher-Order Formulas
    Jasmin Christian Blanchette and Alexander Krauss. Report, Institute for Informatics, T.U. München, January 2010.
    PDF
  • An Isabelle/HOL formalization of the textbook proof of Huffman's algorithm
    Jasmin Christian Blanchette. In Gerwin Klein, Tobias Nipkow, and Larry Paulson, editors, Archive of Formal Proofs, October 2008.
    Web page ⋅ PDF
  • The Little Manual of API Design
    Jasmin Blanchette. Trolltech, a Nokia company, June 2008.
    PDF
  • Verification of Assertions in Creol Programs
    Jasmin Christian Blanchette. Master's thesis, Department of Informatics, University of Oslo, May 2008.
    PDF
  • Overview of the Creol Language
    Jasmin Christian Blanchette. Essay, Department of Informatics, Univerity of Oslo, May 2007.
    PDF
  • Throwing MFC out of Windows—Qt application development with Visual Studio .NET
    Jasmin Blanchette. Linux Magazine 73, pp. 40–43, December 2006.
    Web page ⋅ PDF
  • Windows-to-Linux migration with Qt
    Jasmin Blanchette. TUX 4, July 2005.
    Web page ⋅ PDF

Software
  • DiffPDF—A utility to compare PDFs. Developed by Mark Summerfield.
    Web page

Video

  • Qt 4 Dance, 2005. Jean-Claude, c'est moi.
    YouTube

Address

J. C. Blanchette
Institut für Informatik
Technische Universität München
Boltzmannstr. 3
85748 Garching
Germany

Phone: +49 (0)89 289 17332
Fax: +49 (0)89 289 17307
Email: blanchette the at sign in.tum.de

Office: 01.11.055



“Coinduction is cointuitive.”
— Makarius Wenzel