Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Jasmin Christian Blanchette
[go: Go Back, main page]

Jasmin Christian Blanchette
ジャスミン・クリスチャン・ブランチェット
 

I am a member of the Theorem Proving Group lead by Tobias Nipkow at the Technische Universität München, which I joined in 2008. My research focuses on the generation of counterexamples for higher-order logic (Nitpick) and the use of first-order automatic theorem provers in a higher-order theorem prover (Sledgehammer). I am financed by the project Quis Custodiet (DFG Ni 491/11-2) and affiliated to Programm- und Modell-Analyse. From 2000 to 2008, I worked as software engineer and documentation manager for Trolltech (now Nokia's Qt Development Frameworks) in Oslo, Norway.


Drafts

  • Extending Sledgehammer with SMT solvers
    J. C. B., Sascha Böhme, and Lawrence C. Paulson. Extended version of CADE-23 paper.
    Submitted version (PDF)
  • Monotonicity or how to encode polymorphic types safely and efficiently
    J. C. B., Sascha Böhme, and Nicholas Smallbone.
    Draft (PDF)
  • TFF1: The TPTP typed first-order form with rank-1 polymorphism
    J. C. B. and Andrei Paskevich.
    Draft (PDF)

Journal Articles

  • Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions
    J. C. B. To appear in a special issue of the Software Quality Journal.
    Web page ⋅ Preprint (PDF)
  • Monotonicity inference for higher-order formulas
    J. C. B. and Alexander Krauss. Journal of Automated Reasoning 47(4), pp. 369–398, 2011.
    Web page ⋅ Preprint (PDF)
  • Proof pearl: Mechanizing the textbook proof of Huffman's algorithm in Isabelle/HOL
    J. C. B. Journal of Automated Reasoning 43(1), pp. 1–18, 2009.
    Web page ⋅ Preprint (PDF)

Conference Papers

  • More SPASS with Isabelle—Superposition with hard sorts and configurable simplification
    J. C. B., Andrei Popescu, Daniel Wand, and Christoph Weidenbach. Accepted at Third International Conference on Interactive Theorem Proving (ITP 2012).
    Preprint (PDF)
  • Foundational, compositional (co)datatypes for higher-order logic—Category theory applied to theorem proving
    Dmitriy Traytel, Andrei Popescu, and J. C. B. Accepted at Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2012).
    Preprint (PDF)
  • Automatic proof and disproof in Isabelle/HOL
    J. C. B., Lukas Bulwahn, and Tobias Nipkow. In Tinelli, C., Sofronie-Stokkermans, V. (eds.) 8th International Symposium Frontiers of Combining Systems (FroCoS 2011), LNAI 6989, pp. 12–27, Springer, 2011.
    Web page ⋅ Preprint (PDF)
  • Extending Sledgehammer with SMT solvers
    J. C. B., Sascha Böhme, and Lawrence C. Paulson. In Bjørner, N., Sofronie-Stokkermans, V. (eds.) 23rd International Conference on Automated Deduction (CADE 2011), LNAI 6803, pp. 116–130, Springer, 2011.
    Web page ⋅ Preprint (PDF)
  • Nitpicking C++ concurrency
    J. C. B., Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar. 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011), pp. 113–124, ACM Press, 2011.
    Preprint (PDF)
  • Generating counterexamples for structural inductions by exploiting nonstandard models
    J. C. B. and Koen Claessen. In Fermüller, C. G., Voronkov, A. (eds.) 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR Yogyakarta 2010), LNAI 6397, pp. 117–141, Springer, 2010.
    Web page ⋅ Preprint (PDF)
  • Nitpick: A counterexample generator for Isabelle/HOL based on the relational model finder Kodkod (system description)
    J. C. B. Presented at the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR Yogyakarta 2010).
    Preprint (PDF)
  • Monotonicity inference for higher-order formulas
    J. C. B. and Alexander Krauss. In Giesl, J., Hähnle, R. (eds.) 5th International Joint Conference on Automated Reasoning (IJCAR 2010), LNAI 6173, pp. 91–106, Springer, 2010.
    Web page ⋅ Preprint (PDF)
  • Nitpick: A counterexample generator for higher-order logic based on a relational model finder
    J. C. B. and Tobias Nipkow. In Kaufmann, M., Paulson, L. C. (eds.) First International Conference on Interactive Theorem Proving (ITP 2010), LNCS 6172, pp. 131–146, Springer, 2010.
    Web page ⋅ Preprint (PDF)
  • Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions
    J. C. B. In Fraser, G., Gargantini, A. (eds.) Fourth International Conference on Tests and Proofs (TAP 2010), LNCS 6143, pp. 117–134, Springer, 2010.
    Web page ⋅ Preprint (PDF)
  • Nitpick: A counterexample generator for higher-order logic based on a relational model finder (extended abstract)
    J. C. B. and Tobias Nipkow. Third International Conference on Tests and Proofs (TAP 2009). In Dubois, C. (ed.) TAP 2009: Short Papers, ETH Technical Report 630, 2009.
    Full proceedings (PDF) ⋅ Preprint (PDF)

Workshop Papers

  • Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers
    Lawrence C. Paulson and J. C. B. Invited talk at the 8th International Workshop on the Implementation of Logics (IWIL-2010).
    Full proceedings (PDF) ⋅ Preprint (PDF)
  • Intra-object versus inter-object: Concurrency and reasoning in Creol
    Einar Broch Johnsen, J. C. B., Marcel Kyas, and Olaf Owe. Electronic Notes in Theoretical Computer Science 243 (2nd International Workshop on Harnessing Theories for Tool Support in Software, TTSS 2008), pp. 89–103, 2009.
    Web page ⋅ Preprint (PDF)
  • An open system operational semantics for an object-oriented and component-based language
    J. C. B. and Olaf Owe. Electronic Notes in Theoretical Computer Science 215 (4th International Workshop on Formal Aspects of Component Software, FACS 2007), pp. 151–169, 2008.
    Web page ⋅ Preprint (PDF)

Theses

  • Automatic Proofs and Refutations for Higher-Order Logic
    J. C. B. Ph.D. thesis, Fakultät für Informatik, Technische Universität München, June 2012.
    PDF
  • Verification of Assertions in Creol Programs
    J. C. B. M.Sc. thesis, Institutt for informatikk, Universitetet i Oslo, May 2008.
    PDF

Books

  • C++ GUI Programming with Qt 4 (Second Edition)
    J. B. 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
    J. B. 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
    J. B. 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

  • An Isabelle/HOL formalization of the textbook proof of Huffman's algorithm
    J. C. B. In Gerwin Klein, Tobias Nipkow, and Larry Paulson, editors, Archive of Formal Proofs, October 2008.
    Web page ⋅ PDF
  • The Little Manual of API Design
    J. B. Trolltech, a Nokia company, June 2008.
    PDF
  • Overview of the Creol Language
    J. C. B. Essay, Department of Informatics, Univerity of Oslo, May 2007.
    PDF
  • Throwing MFC out of Windows—Qt application development with Visual Studio .NET
    J. B. Linux Magazine 73, pp. 40–43, December 2006.
    Web page ⋅ PDF
  • Windows-to-Linux migration with Qt
    J. B. TUX 4, July 2005.
    Web page ⋅ PDF

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

Activities


Video

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

Address

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

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

Office: 01.11.060



“A proof is a proof.
What kind of a proof?
It's a proof.
A proof is a proof,
and when you have a good proof,
it's because it's proven.”

— Jean Chrétien