Nothing Special   »   [go: up one dir, main page]
Links und Funktionen
Inhaltsbereich
Bio | News | Teaching | Team | Publications | Formal Proofs | Software | Activities | Media | Contact

Prof. Dr. Jasmin Blanchette Prof. Dr. Jasmin Blanchette

I am a professor of Theoretical Computer Science and Theorem Proving at Ludwig-Maximilians-Universität München, where I serve as the Dean of Studies for Computer Science. I am also a guest researcher in the VeriDis group at Loria in Nancy and in the Automation of Logic group at Max-Planck-Institut für Informatik in Saarbrücken.

Theorem proving plays a central role in formal methods and, more generally, in theoretical computer science. With my research, I aim at strengthening proof automation for general-purpose logics and making proof assistants more cost-effective to use. A hallmark of my research is the combination of automatic and interactive methods—of human and artificial intelligence. I envision a future in which automatic theorem provers and proof assistants will be routinely used for critical computing infrastructure, for programming language design, and more broadly for research in computer science and mathematics, thereby leading to more trustworthy systems and science.

Specifically, my research focuses on the development and use of automatic theorem provers and model finders to find proofs and counterexamples in higher-order logic (with tools such as Sledgehammer and Nitpick and projects such as Matryoshka and Nekoka). I am also interested in formalizing classic results and modern research in automated reasoning (IsaFoL) and number theory (Lean Forward). Finally, I develop foundational definitional mechanisms for (co)datatypes and (co)recursive functions.

News

Teaching

Team

At Ludwig-Maximilians-Universität München

At Other Institutes

  • Martin Desharnais (PhD student, formalization of logic; cosupervisors: Christoph Weidenbach, Sophie Tourret)
  • Martin Dvorak (PhD student, formalization of Chomsky hierarchy in Lean; cosupervisor: Vladimir Kolmogorov)
  • Vincent Fischer (PhD student, TBD; cosupervisor: Javier Esparza)
  • Visa Nummelin (PhD student, reasoning about higher-order logic and Booleans; cosupervisor: Sander Dahmen)

Past Members

  • Anne Baanen (PhD student, formalization of number theory; cosupervisor: Sander Dahmen)
  • Alexander Bentkamp (PhD student and postdoc, higher-order superposition)
  • Simon Cruanes (senior software engineer, counterexample generation)
  • Rosalie Defourné (PhD student, hammer for TLAPS; cosupervisors: Stephan Merz, Pascal Fontaine)
  • Gabriel Ebner (postdoc, Lean development and clause splitting)
  • Daniel El Ouraoui (PhD student, higher-order SMT; cosupervisors: Stephan Merz, Pascal Fontaine)
  • Michael Färber (postdoc, nonclausal theorem proving and connection calculus)
  • Mathias Fleury (PhD student, formalization of inference systems; cosupervisor: Christoph Weidenbach)
  • Johannes Hölzl (postdoc, formalization of mathematics)
  • Robert Y. Lewis (postdoc, tool support for formalizing mathematics)
  • Anders Schlichtkrull (PhD student, formalization of logical calculi; cosupervisors: Jørgen Villadsen, Thomas Bolander)
  • Hans-Jörg Schurr (PhD student, higher-order SMT; cosupervisors: Stephan Merz, Pascal Fontaine)
  • Petar Vukmirović (PhD student, implementation of higher-order superposition; cosupervisors: Wan Fokkink, Stephan Schulz)
  • Daniel Wand (PhD student, extensions of superposition; cosupervisor: Christoph Weidenbach)

Publications

Draft

  • Augmenting Model-Based Instantiation with Fast Enumeration. Lydia Kondylidou, Jasmin Blanchette, and Andrew Reynolds. Authors’ PDF

2024

  • A modular formalization of superposition in Isabelle/HOL. Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. In Bertot, Y., Kutsia, T., Norrish. M. 15th International Conference on Interactive Theorem Proving (ITP 2024), LIPIcs 309, pages 12:1-12:20, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2024. Publisher’s page ⋅ Authors’ PDF
  • The Hitchhiker’s Guide to Logical Verification. Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Jannis Limperg, and Johannes Hölzl. 2024. PDF (desktop) ⋅ PDF (tablet)
  • Huffman’s algorithm. Jasmin Blanchette. In Nipkow, T., Functional Data Structures and Algorithms: A Proof Assistant Approach, 2024. Editor’s PDF

2023

  • Complete and efficient higher-order reasoning via lambda-superposition. Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, and Uwe Waldmann. ACM SIGLOG News 10(4): 25-40, 2023. Publishers’ page ⋅ Authors’ PDF
  • Recurrence-driven summations in automated deduction. Visa Nummelin, Jasmin Blanchette, and Sander R. Dahmen. In Sattler, U., Suda, M. 14th International Symposium on Frontiers of Combining Systems (FroCoS 2023), LNCS 14279, pp. 23–40, Springer, 2023. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • λ-Superposition: from theory to trophy. Jasmin Blanchette. In Pientka, B., Tinelli, C. 29th International Conference on Automated Deduction (CADE-29), LNCS 14132, pp. xiii–xvi, Springer, 2023. Publisher’s PDF ⋅ Author’s PDF
  • Verified given clause procedures. Jasmin Blanchette, Qi Qiu, and Sophie Tourret. In Pientka, B., Tinelli, C. 29th International Conference on Automated Deduction (CADE-29), LNCS 14132, pp. 61–77, Springer, 2023. Publisher’s page ⋅ Authors’ PDF
  • Closure properties of general grammars—formally verified Martin Dvorak and Jasmin Blanchette. In Naumowicz, A., Thiemann, R. 14th International Conference on Interactive Theorem Proving (ITP 2023), LIPIcs 268, pages 11:1-11:16, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2023. Publisher’s page ⋅ Authors’ PDF
  • Finding mathematical proofs using computers. Alexander Bentkamp and Jasmin Blanchette. Nieuw Archief voor Wiskunde 5/24(2): 114–118, 2023. Publisher’s PDF ⋅ Authors’ PDF
  • Workshop Papers at 14th Conference on Intelligent Computer Mathematics (CICM 2021). Jasmin Blanchette, James Davenport, Peter Koepke, Andrea Kohlhase, Michael Kohlhase, Adam Naumowicz, Dennis Müller, Yasmine Sharoda, and Claudio Sacerdoti Coen (eds.). CEUR-WS 3377, 2023. Publisher’s page
  • SAT-inspired higher-order eliminations. Jasmin Blanchette and Petar Vukmirović. Logical Methods in Computer Science 19(2), 2023. Publisher’s page ⋅ Authors’ PDF
  • SAT-inspired eliminations for superposition. Petar Vukmirović, Jasmin Blanchette, and Marijn J.H. Heule. Transactions on Computational Logic 24(1): article 7, 2023. Publisher’s page ⋅ Authors’ PDF
  • Unifying splitting. Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret. Journal of Automated Reasoning 67, article number 16, 2023. Publisher’s page ⋅ Authors’ PDF
  • Mechanical mathematicians. Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Communications of the ACM 66(4): 80–90, 2023. Publisher’s page ⋅ Authors’ PDF
  • Superposition for higher-order logic. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. Journal of Automated Reasoning 67, article number 10, 2023. Publisher’s page ⋅ Authors’ PDF ⋅ Errata (PDF)
  • Extending a high-performance prover to higher-order logic. Petar Vukmirović, Jasmin Blanchette, and Stephan Schulz. 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), LNCS 13994, pp. 111–129, Springer, 2023. Publisher’s page ⋅ Authors’ PDF

2022

  • A comprehensive framework for saturation theorem proving. Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. Journal of Automated Reasoning 66(4): 499–539, 2022. Publisher’s page ⋅ Authors’ PDF
  • Making higher-order superposition work. Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Journal of Automated Reasoning 66(4): 541–564, 2022. Publisher’s page ⋅ Authors’ PDF
  • 11th International Joint Conference on Automated Reasoning (IJCAR 2022). Jasmin Blanchette, Laura Kovács, and Dirk Pattinson (eds.). LNCS 13385, Springer, 2022. Publisher’s page
  • Seventeen provers under the hammer. Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. In Andronick, J., de Moura, L. (ed.) 13th Conference on Interactive Theorem Proving (ITP 2022), LIPIcs 237, pages 8:1–8:18, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2022. Publisher’s page ⋅ Authors’ PDF
  • Extending a brainiac prover to lambda-free higher-order logic. Petar Vukmirović, Jasmin Blanchette, Simon Cruanes, and Stephan Schulz. International Journal on Software Tools for Technology Transfer 24(1): 67–87, 2022. Publisher’s page ⋅ Authors’ PDF

2021

  • Superposition with lambdas. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Journal of Automated Reasoning 65(7): 893–940, 2021. Publisher’s page ⋅ Authors’ PDF
  • SAT-inspired eliminations for superposition. Petar Vukmirović, Jasmin Blanchette, and Marijn J.H. Heule. In Piskac, R., Whalen, M. (eds.) 21st International Conference on Formal Methods in Computer-Aided Design (FMCAD 2021), pp. 231–240, IEEE, 2021. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Superposition for lambda-free higher-order logic. Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann. Logical Methods in Computer Science 17(2), pp. 1:1–1:38, 2021. Publisher’s page ⋅ Authors’ PDF
  • A unifying splitting framework. Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS 12699, pp. 344–360, Springer, 2021. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Superposition for full higher-order logic. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS 12699, pp. 396–412, Springer, 2021. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF) ⋅ Errata (PDF)
  • Making higher-order superposition work. Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS 12699, pp. 415–432, Springer, 2021. Publisher’s page ⋅ Authors’ PDF
  • A modular Isabelle framework for verifying saturation provers. Sophie Tourret and Jasmin Blanchette. In Hrițcu, C., Popescu, A. (eds.) 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), pp. 224–237, ACM, 2021. Publisher’s page ⋅ Authors’ PDF

2020

  • A comprehensive framework for saturation theorem proving. Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. In Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Part I, LNCS 12166, pp. 316–334, Springer, 2020. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Formalizing Bachmair and Ganzinger’s ordered resolution prover. Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, and Uwe Waldmann. Journal of Automated Reasoning 64(7): 1169–1195, 2020. Online viewer ⋅ Publisher’s page ⋅ Authors’ PDF
  • Scalable fine-grained proofs for formula processing. Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, and Pascal Fontaine. Journal of Automated Reasoning 64(3): 485–510, 2020. Online viewer ⋅ Publisher’s page ⋅ Authors’ PDF
  • 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020). Jasmin Blanchette and Cătălin Hrițcu (eds.). ACM, 2020. Publisher’s page

2019

  • Superposition with lambdas. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 55–73, Springer, 2019. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Extending a brainiac prover to lambda-free higher-order logic. Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, and Stephan Schulz. In Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), LNCS 11427, pp. 192–210, Springer, 2019. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • A verified prover based on ordered resolution. Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), pp. 152–165, ACM, 2019. Publisher’s page ⋅ Authors’ PDF
  • Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). Jasmin Christian Blanchette. In Mahboubi, A., Myreen, M. O. (eds.) 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), pp. 1–13, ACM, 2019. Publisher’s page ⋅ Author’s PDF
  • Bindings as bounded natural functors. Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. In PAMPL 3(POPL), pp. 22:1–22:34, 2019. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • A formal proof of the expressiveness of deep learning. Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Journal of Automated Reasoning 63(2), pp. 347–368, 2019. Online viewer ⋅ Publisher’s page ⋅ Authors’ PDF
  • Stronger higher-order automation: A report on the ongoing Matryoshka project. Jasmin Blanchette, Pascal Fontaine, Stephan Schulz, Sophie Tourret, and Uwe Waldmann. Presented at 2nd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019). Authors’ PDF
  • Better SMT proofs for easier reconstruction. Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine, and Hans-Jörg Schurr. In Hales, T. C., Kaliszyk, C., Kumar, R., Schulz, S., Urban, J. (eds.) 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019). Authors’ PDF
  • Machine learning for instance selection in SMT solving. Jasmin Christian Blanchette, Daniel El Ouraoui, Pascal Fontaine, and Cezary Kaliszyk. In Hales, T. C., Kaliszyk, C., Kumar, R., Schulz, S., Urban, J. (eds.) 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019). Authors’ PDF

2018

  • Superposition with datatypes and codatatypes. Jasmin Christian Blanchette, Nicolas Peltier, and Simon Robillard. In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018), LNCS 10900, pp. 370–387, Springer, 2018. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Superposition for lambda-free higher-order logic. Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann. In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018), LNCS 10900, pp. 28–46, Springer, 2018. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Formalizing Bachmair and Ganzinger’s ordered resolution prover. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann. In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018), LNCS 10900, pp. 89–107, Springer, 2018. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • A verified SAT solver with watched literals using Imperative HOL. Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. In Andronick, J., Felty, A. P. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 158–171, ACM, 2018. Publisher’s page ⋅ Authors’ PDF
  • A verified SAT solver framework with learn, forget, restart, and incrementality. Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. Journal of Automated Reasoning 61(1–4), pp. 333–365, 2018. Online viewer ⋅ Publisher’s page ⋅ Authors’ PDF
  • Introduction to Milestones in Interactive Theorem Proving. Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence Paulson, Andrei Popescu, and Gregor Snelting. Journal of Automated Reasoning 61(1–4), pp. 1–8, 2018. Publisher’s page ⋅ Authors’ PDF
  • A verified prover based on ordered resolution. Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. In Krebbers, R., Swierstra, W., and Visser, E. (eds.) 1st VERSEN Workshop on Programming Languages in the Netherlands (PLNL 2018). Web page
  • A verified SAT solver with watched literals using Imperative HOL (extended abstract). Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. In Nipkow, T., Paulson, L., Wenzel, M. (eds.) Isabelle Workshop 2018. Authors’ PDF

2017

  • Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. In Miller, D. (ed.) 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), LIPIcs 84, pages 11:1–11:18, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2017. Publisher’s page ⋅ Authors’ PDF
  • A formal proof of the expressiveness of deep learning. Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. In Ayala-Rincón, M., Muños, C. A. (eds.) 8th Conference on Interactive Theorem Proving (ITP 2017), LNCS 10499, pp. 46–64, Springer, 2017. Publisher’s page ⋅ Authors’ PDF
  • A verified SAT solver framework with learn, forget, restart, and incrementality. Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach. In Sierra, C. (ed.) 26th International Joint Conference on Artificial Intelligence (IJCAI-17), pp. 4786–4790, ijcai.org, 2017. Publisher’s page ⋅ Authors’ PDF
  • Foundational (co)datatypes and (co)recursion for higher-order logic. Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel. In Dixon, C., Finger, M. (eds.) 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), LNCS 10483, pp. 3–21, Springer, 2017. Publisher’s page ⋅ Authors’ PDF
  • A transfinite Knuth–Bendix order for lambda-free higher-order terms. Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE-26), LNCS 10395, pp. 432–453, Springer, 2017. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Scalable fine-grained proofs for formula processing. Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine. In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE-26), LNCS 10395, pp. 398–412, Springer, 2017. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Foundational nonuniform (co)datatypes for higher-order logic. Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, and Dmitriy Traytel. 32nd Annual IEEE Symposium on Logic in Computer Science (LICS 2017), pp. 1–12, IEEE Computer Society, 2017. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • A lambda-free higher-order recursive path order. Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. In Esparza, J., Murawski, A. S. (eds.) 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), LNCS 10203, pp. 461–479, Springer, 2017. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Friends with benefits: Implementing corecursion in foundational proof assistants. Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. In Yang, H. (ed.) 26th European Symposium on Programming (ESOP 2017), LNCS 10201, pp. 111–140, Springer, 2017. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • A decision procedure for (co)datatypes in SMT solvers. Andrew Reynolds and Jasmin Christian Blanchette Journal of Automated Reasoning 58(3), pp. 341–362, 2017. Online viewer ⋅ Publisher’s page ⋅ Authors’ PDF
  • Soundness and completeness proofs by coinductive methods. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Journal of Automated Reasoning 58(1), pp. 149–179, 2017. Online viewer ⋅ Publisher’s page ⋅ Authors’ PDF

  • Towards strong higher-order automation for fast interactive verification. Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, and Uwe Waldmann. In Reger, G., Traytel, D. (eds.) 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2017), pp. 16–23, EPiC 51, EasyChair, 2017. Publisher’s page ⋅ Authors’ PDF

  • Language and proofs for higher-order SMT (work in progress). Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, and Pascal Fontaine. In Dubois, C., Woltzenlogel Paleo, B. (eds.) 5th Workshop on Proof eXchange for Theorem Proving (PxTP 2017), pp. 15–22, EPTCS 262, 2017. Publisher’s page ⋅ Authors’ PDF
  • An Isabelle formalization of the expressiveness of deep learning (extended abstract). Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. In Hales, T. C., Kaliszyk, C., Schulz, S., Urban, J. (eds.) 2nd Conference on Artificial Intelligence and Theorem Proving (AITP 2017), pp. 22–23. Authors’ PDF

2016

  • A decision procedure for (co)datatypes in SMT solvers. Andrew Reynolds and Jasmin Christian Blanchette. In Kambhampati, S. (ed.) 25th International Joint Conference on Artificial Intelligence (IJCAI-16), pp. 4205–4209, IJCAI/AAAI Press, 2016. Publisher’s page ⋅ Authors’ PDF
  • A verified SAT solver framework with learn, forget, restart, and incrementality. Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach. In Olivetti, N., Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016), LNCS 9706, pp. 25–44, Springer, 2016. Publisher’s page ⋅ Authors’ PDF
  • Model finding for recursive functions in SMT. Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, and Cesare Tinelli. In Olivetti, N., Tiwari, A. (eds.) 8th International Joint Conference on Automated Reasoning (IJCAR 2016), LNCS 9706, pp. 133–151, Springer, 2016. Publisher’s page ⋅ Authors’ PDF
  • Encoding monomorphic and polymorphic types. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. Logical Methods in Computer Science 12(4), pp. 13:1–13:52, 2016. Publisher’s page ⋅ Authors’ PDF
  • A learning-based fact selector for Isabelle/HOL. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. Journal of Automated Reasoning 57(3), pp. 219–244, 2016. Online viewer ⋅ Publisher’s page ⋅ Authors’ PDF
  • Semi-intelligible Isar proofs from machine-generated proofs. Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier. Journal of Automated Reasoning 56(2), pp. 155–200, 2016. Publisher’s page ⋅ Authors’ PDF
  • Hammering towards QED. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Journal of Formalized Reasoning 9(1), pp. 101–148, 2016. Publisher’s page ⋅ Authors’ PDF
  • Extending Nunchaku to dependent type theory. Simon Cruanes and Jasmin Christian Blanchette Hammers for Type Theories (HaTT 2016) Publisher’s page ⋅ Authors’ PDF
  • My life with an automatic theorem prover. Jasmin Christian Blanchette In Kovács, L., Voronkov, A. (eds.) 1st and 2nd Vampire Workshops (Vampire 2014 and 2015), pp. 1–7, EPiC 38, EasyChair, 2016. Authors’ PDF
  • Friends with benefits: Implementing foundational corecursion in Isabelle/HOL (extended abstract). Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. Isabelle Workshop 2016. Authors’ PDF
  • A verified SAT solver framework with learn, forget, restart, and incrementality (extended abstract). Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach. Isabelle Workshop 2016. Authors’ PDF
  • 7th International Conference on Interactive Theorem Proving (ITP 2016). Jasmin Christian Blanchette and Stephan Merz (eds.). LNCS 9807, Springer, 2016. Publisher’s page
  • 1st International Workshop on Hammers for Type Theories (HaTT 2016). Jasmin Christian Blanchette and Cezary Kaliszyk (eds.). EPTCS 210, 2016. Publisher’s page ⋅ Authors’ PDF

2015

  • Foundational extensible corecursion: A proof assistant perspective. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. In Fisher, K., Reppy, J. H. (eds.) 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 192–204, ACM, 2015. Publisher’s page ⋅ Authors’ PDF
  • A decision procedure for (co)datatypes in SMT solvers. Andrew Reynolds and Jasmin Christian Blanchette In Felty, A., Middeldorp, A. (eds.) 25th International Conference on Automated Deduction (CADE-25), LNCS 9195, pp. 197–213, Springer, 2015. Publisher’s page ⋅ Authors’ PDF ⋅ Report (PDF)
  • Mining the Archive of Formal Proofs. Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. In Kerber, M. (ed.) International Conference on Intelligent Computer Mathematics (CICM 2015), LNCS 9150, pp. 1–15, Springer, 2015. Publisher’s page ⋅ Authors’ PDF
  • Witnessing (co)datatypes. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. In Vitek, J. (ed.)European Symposium on Programming (ESOP 2015), LNCS 9032, pp. 359–382, Springer, 2015. Publisher’s page ⋅ Authors’ PDF
  • Model finding for recursive functions in SMT. Andrew Reynolds, Jasmin Christian Blanchette, and Cesare Tinelli. In Ganesh, V., Jovanović, D. (eds.) Satisfiability Modulo Theories Workshop (SMT 2015). Authors’ PDF ⋅ Report (PDF)
  • Model finding for recursive functions in SMT. Andrew Reynolds, Jasmin Christian Blanchette, and Cesare Tinelli. QUANTIFY 2015. Authors’ PDF
  • Toward Nitpick and Sledgehammer for Coq. Jasmin Christian Blanchette. Coq Workshop 2015. Author’s PDF
  • Isabelle and security. Jasmin Christian Blanchette and Andrei Popescu. Grande Region Security and Reliability Day 2015, presented at poster session. Authors’ PDF
  • 9th International Conference on Tests and Proofs (TAP 2015). Jasmin Christian Blanchette and Nikolai Kosmatov (eds.). LNCS 9154, Springer, 2015. Publisher’s page

2014

  • Experience report: The next 1100 Haskell programmers. Jasmin Christian Blanchette, Lars Hupel, Tobias Nipkow, Lars Noschinski, and Dmitriy Traytel. In Jeuring, J., Chakravarty, M. M. T. (eds.) ACM SIGPLAN Haskell Symposium 2014 (Haskell 2014), pp. 25–30, ACM, 2014. Publisher’s page ⋅ Authors’ PDF
  • Truly modular (co)datatypes for Isabelle/HOL. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. In Klein, G., Gamboa, R. (eds.)5th Conference on Interactive Theorem Proving (ITP 2014), LNCS 8558, pp. 93–110, Springer, 2014. Publisher’s page ⋅ Authors’ PDF
  • Cardinals in Isabelle/HOL. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. In Klein, G., Gamboa, R. (eds.)5th Conference on Interactive Theorem Proving (ITP 2014), LNCS 8558, pp. 111–127, Springer, 2014. Publisher’s page ⋅ Authors’ PDF
  • Unified classical logic completeness: A coinductive pearl. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. In Demri, S., Kapur, D., Weidenbach, C. (eds.) 7th International Joint Conference on Automated Reasoning (IJCAR 2014), LNCS 8562, pp. 46–60, Springer, 2014. Publisher’s page ⋅ Authors’ PDF
  • Primitively (co)recursive definitions for Isabelle/HOL. Lorenz Panny, Jasmin Christian Blanchette, and Dmitriy Traytel. Isabelle Workshop 2014. Authors’ PDF
  • A survey of axiom selection as a machine learning problem. Jasmin Christian Blanchette and Daniel Kühlwein. In Geschke, S., Loewe, B., Schlicht, P. (eds.) Infinity, Computability, and Metamathematics: Festschrift Celebrating the 60th Birthdays of Peter Koepke and Philip Welch, Tributes, College Publications, 2014. Authors’ PDF

2013

  • Mechanizing the metatheory of Sledgehammer. Jasmin Christian Blanchette and Andrei Popescu. In Fontaine, P., Ringeissen, C., Schmidt, R. A. (eds.)9th International Symposium on Frontiers of Combining Systems (FroCoS 2013), LNCS 8152, pp. 245–260, Springer, 2013. Publisher’s page ⋅ Authors’ PDF
  • MaSh: Machine learning for Sledgehammer. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. In Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.)4th Conference on Interactive Theorem Proving (ITP 2013), LNCS 7998, pp. 35–50, Springer, 2013. Publisher’s page ⋅ Authors’ PDF
  • TFF1: The TPTP typed first-order form with rank-1 polymorphism. Jasmin Christian Blanchette and Andrei Paskevich. In Bonacina, M. P. (ed.) 24th International Conference on Automated Deduction (CADE-24), LNCS 7898, pp. 414–420, Springer, 2013. Publisher’s page ⋅ Authors’ PDF ⋅ Specification (PDF)
  • Encoding monomorphic and polymorphic types. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. In Piterman, N., Smolka, S. (eds.) 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), LNCS 7795, pp. 493–507, Springer, 2013. Publisher’s page ⋅ Authors’ PDF
  • Extending Sledgehammer with SMT solvers. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Journal of Automated Reasoning 51(1), pp. 109–128, 2013. Publisher’s page ⋅ Authors’ PDF
  • LEO-II and Satallax on the Sledgehammer test bench. Nik Sultana, Jasmin Christian Blanchette, and Lawrence C. Paulson. Journal of Applied Logic 11(1), pp. 91–102, 2013. Publisher’s page ⋅ Authors’ PDF
  • Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions. Jasmin Christian Blanchette. Software Quality Journal 21(1), pp. 101–126, 2013. Publisher’s page ⋅ Author’s PDF
  • Robust, semi-intelligible Isabelle proofs from ATP proofs. Steffen Juilf Smolka and Jasmin Christian Blanchette. In Blanchette, J. C., Urban, J. (eds.) 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), pp. 117–132, EPiC 14, EasyChair, 2013. Publisher’s page ⋅ Authors’ PDF
  • Redirecting proofs by contradiction. Jasmin Christian Blanchette. In Blanchette, J. C., Urban, J. (eds.) 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), pp. 11–26, EPiC 14, EasyChair, 2013. Publisher’s page ⋅ Authors’ PDF
  • 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP 2013). Jasmin Christian Blanchette and Josef Urban (eds.). EPiC 14, EasyChair, 2013. Publisher’s page ⋅ Authors’ PDF

2012

  • Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette In_27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012)_, pp. 596–605, IEEE Computer Society, 2012. Publisher’s page ⋅ Authors’ PDF
  • More SPASS with Isabelle: Superposition with hard sorts and configurable simplification. Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach. In Beringer, L., Felty, A. P. (eds.) 3rd International Conference on Interactive Theorem Proving (ITP 2012), LNCS 7406, pp. 345–360, Springer, 2012. Publisher’s page ⋅ Authors’ PDF
  • Automatic Proofs and Refutations for Higher-Order Logic. Jasmin Christian Blanchette PhD thesis, Fakultät für Informatik, Technische Universität München, June 2012. Author’s PDF

2011

  • Monotonicity inference for higher-order formulas. Jasmin Christian Blanchette and Alexander Krauss. Journal of Automated Reasoning 47(4), pp. 369–398, 2011. Publisher’s page ⋅ Authors’ PDF
  • Automatic proof and disproof in Isabelle/HOL. Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. In Tinelli, C., Sofronie-Stokkermans, V. (eds.) 8th International Symposium Frontiers of Combining Systems (FroCoS 2011), LNCS 6989, pp. 12–27, Springer, 2011. Publisher’s page ⋅ Authors’ PDF
  • Extending Sledgehammer with SMT solvers. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. In Bjørner, N., Sofronie-Stokkermans, V. (eds.) 23rd International Conference on Automated Deduction (CADE-23), LNCS 6803, pp. 116–130, Springer, 2011. Publisher’s page ⋅ Authors’ PDF
  • Nitpicking C++ concurrency. Jasmin Christian Blanchette, 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, 2011. Publisher’s page ⋅ Authors’ PDF

2010

  • Generating counterexamples for structural inductions by exploiting nonstandard models. Jasmin Christian Blanchette 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), LNCS 6397, pp. 117–141, Springer, 2010. Publisher’s page ⋅ Authors’ PDF
  • Nitpick: A counterexample generator for Isabelle/HOL based on the relational model finder Kodkod (system description). Jasmin Christian Blanchette. Presented at the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR Yogyakarta 2010). Publisher’s page ⋅ Authors’ PDF
  • Monotonicity inference for higher-order formulas. Jasmin Christian Blanchette and Alexander Krauss. In Giesl, J., Hähnle, R. (eds.) 5th International Joint Conference on Automated Reasoning (IJCAR 2010), LNCS 6173, pp. 91–106, Springer, 2010. Publisher’s page ⋅ Authors’ PDF
  • Nitpick: A counterexample generator for higher-order logic based on a relational model finder. Jasmin Christian Blanchette and Tobias Nipkow. In Kaufmann, M., Paulson, L. C. (eds.)1st International Conference on Interactive Theorem Proving (ITP 2010), LNCS 6172, pp. 131–146, Springer, 2010. Publisher’s page ⋅ Authors’ PDF
  • Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions. Jasmin Christian Blanchette. In Fraser, G., Gargantini, A. (eds.) 4th International Conference on Tests and Proofs (TAP 2010), LNCS 6143, pp. 117–134, Springer, 2010. Publisher’s page ⋅ Author’s PDF
  • Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. Lawrence C. Paulson and Jasmin Christian Blanchette 8th International Workshop on the Implementation of Logics (IWIL-2010). Full proceedings (PDF) ⋅ Authors’ PDF

2009

  • 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, 2009. Publisher’s page ⋅ Author’s PDF
  • Nitpick: A counterexample generator for higher-order logic based on a relational model finder (extended abstract). Jasmin Christian Blanchette and Tobias Nipkow. In Dubois, C. (ed.) 3rd International Conference on Tests and Proofs (TAP 2009): Short Papers, ETH Technical Report 630, 2009. Full proceedings (PDF) ⋅ Authors’ PDF
  • Intra-object versus inter-object: Concurrency and reasoning in Creol. Einar Broch Johnsen, Jasmin Christian Blanchette, 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. Publisher’s page ⋅ Authors’ PDF

2008

  • 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 (4th International Workshop on Formal Aspects of Component Software, FACS 2007), pp. 151–169, 2008. Publisher’s page ⋅ Authors’ PDF
  • The Little Manual of API Design. Jasmin Blanchette. Trolltech, a Nokia company, June 2008. Author’s PDF
  • Verification of Assertions in Creol Programs. Jasmin Christian Blanchette MSc thesis, Institutt for informatikk, Universitetet i Oslo, May 2008. Author’s PDF
  • 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. Publisher’s page

2006

  • 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. Publisher’s page ⋅ Authors’ PDF

2004

  • 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. Publisher’s page ⋅ Authors’ PDF

Formal Proofs

2020

  • Extensions to the comprehensive framework for saturation theorem proving. Jasmin Blanchette and Sophie Tourret. Archive of Formal Proofs, 2020. Web page

2018

  • A verified functional implementation of Bachmair and Ganzinger’s ordered resolution prover. Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. Archive of Formal Proofs, 2018. Web page
  • Formalization of Bachmair and Ganzinger’s ordered resolution prover. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann. Archive of Formal Proofs, 2018. Web page
  • Operations on bounded natural functors. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2018. Web page

2017

  • Abstract soundness. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2017. Web page

2016

  • Formalization of Knuth–Bendix orders for lambda-free higher-order terms. Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. Archive of Formal Proofs, 2016. Web page
  • Formalization of nested multisets, hereditary multisets, and syntactic ordinals. Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Archive of Formal Proofs, 2016. Web page
  • Formalization of recursive path orders for lambda-free higher-order terms. Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. Archive of Formal Proofs, 2016. Web page

2014

  • Abstract completeness. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Archive of Formal Proofs, 2014. Web page

2013

  • Sound and complete sort encodings for first-order logic. Jasmin Christian Blanchette and Andrei Popescu. Archive of Formal Proofs, 2013. Web page

2008

  • The textbook proof of Huffman’s algorithm. Jasmin Christian Blanchette. Archive of Formal Proofs, 2008. Web page

Software

Activities

  • Editor-in-chief of Journal of Automated Reasoning (2021–).
  • Special issue editor: Journal of Automated Reasoning 2019, Software and Systems Modeling 2019.
  • Steering committee member: CPP (2019–2023), CADE trustee (2016–2019, 2021–2022, 2023–), ITP (2016–), TAP (2015–).
  • AAR newsletter editor and board member (2015–2017).
  • Conference program committee member: OOPSLA 2024–25, CPP 2025, LPAR 2024, IJCAR 2024, CICM 2024, AAAI 2024, LPAR 2023, CICM 2023, FMICS 2023, ITP 2023, ITP 2022, IJCAR 2022 (co-chair), TACAS 2022, FroCoS 2021, CADE-28, NFM 2021, ITP 2021, CAV 2021, CSL 2021, LPAR 2020, IJCAR 2020, TAP 2020, TACAS 2020, CPP 2020 (co-chair), FMCAD 2019, PPDP 2019, FroCoS 2019, CADE-27, NFM 2018, CAV 2018, TAP 2018, IJCAR 2018, ITP 2018, CPP 2018, CAV 2017, CADE-26, TAP 2017, ITP 2016 (co-chair), TAP 2016, TAP 2015 (co-chair), CADE-25, IJCAR 2014, FroCoS 2013.
  • Conference organization: ITP 2016 (co-organizer), CADE-25 (co-chair of workshops, tutorials, and competitions).
  • Workshop program committee member: AITP 2024, IWIL-2024, Deduktionstreffen 2023, IWIL-2023, AITP 2023, Deduktionstreffen 2022, AITP 2022, FMM 2021 (co-chair), AITP 2021, IWIL-2020, AITP 2020, ARCADE 2019, Deduktionstreffen 2019, AITP 2019, IWIL-2018, Deduktionstreffen 2018, AITP 2018, SMT 2017, PxTP 2017, IWIL-2017, ARCADE 2017, AITP 2017, Deduktionstreffen 2016, SMT 2016, HaTT 2016 (co-chair), QBF 2016, IWIL-2015, LSFA 2015, QUANTIFY 2015, Deduktionstreffen 2015, PxTP 2015, PAAR-2014, PxTP 2013 (co-chair), PxTP 2012, IWIL-2012, PAAR-2012, and IWIL-2010.
  • Workshop organization: DeMent 2020 (canceled), DeMent 2019, VeriDis Retreat + Matryoshka 2019, VDMW 2018, WAIT 2018, Matryoshka 2018.

Media

  • Dutch Prize for ICT research 2022 winner Jasmin Blanchette, 2022. YouTube
  • I/O magazine, April 2022. Driven to Develop Correct Software. By Bennie Mols. Pages 16–17. Issue (PDF)
  • I/O magazine, April 2019. Computer houdt wiskundigen op het rechte pad. By Bennie Mols. Pages 22–24. Issue (PDF)
  • Inria Inside—Jasmin Blanchette, 2016. YouTube
  • Qt 4 Dance, 2005. Jean-Claude, c’est moi. YouTube

Contact

Prof. Dr. Jasmin Blanchette
Lehr- und Forschungseinheit für Theoretische Informatik und Theorembeweisen
Institut für Informatik
Ludwig-Maximilians-Universität München
Oettingenstr. 67
80538 München
Germany

Room: L 107 Phone: +49 (0)89 2180 9337 (secretary)
Email: jasmin.blanchette shtrudel ifi.lmu.de
Email (as Dean of Studies): studiendekan shtrudel ifi.lmu.de

“After many years I’ve finally come to realize that my main strength lies in an ability to delegate work and to lead large projects, rather than to go it alone. Programming has never really been my forte.” — Donald E. Knuth

Artikelaktionen

Funktionsleiste