Jasmin Blanchette

46 papers A 7B 8Journal 22Unranked 7
YearRankTypeTitle / Venue / Authors
2026 B conf
Adding Sorts to an Isabelle Formalization of Superposition.
CPP
Balázs Tóth, Martin Desharnais-Schäfer, Jasmin Blanchette
2026 — conf
Enumerating Choice Terms in Model-Based Quantifier Instantiation.
TACAS (1)
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, Cesare Tinelli
2025 — conf
Augmenting Model-Based Instantiation with Fast Enumeration.
TACAS (1)
Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette
2025 A conf
Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL.
CADE
Lukas Bartl, Jasmin Blanchette, Tobias Nipkow
2025 J jnl
Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL.
CoRR
Lukas Bartl, Jasmin Blanchette, Tobias Nipkow
2025 — conf
Iterative Monomorphisation.
FroCoS
Tanguy Bozec, Jasmin Blanchette
2025 J jnl
Optimistic Higher-Order Superposition.
CoRR
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger, Uwe Waldmann
2025 B conf
Sledgehammering Without ATPs (Short Paper).
ITP
Martin Desharnais, Jasmin Blanchette
2025 J jnl
Term Orders for Optimistic Lambda-Superposition.
CoRR
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger
2024 B conf
A Modular Formalization of Superposition in Isabelle/HOL.
ITP
Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret
2023 B conf
Closure Properties of General Grammars - Formally Verified.
ITP
Martin Dvorak, Jasmin Blanchette
2023 J jnl
Closure Properties of Unrestricted Grammars - Formally Verified.
CoRR
Martin Dvorak, Jasmin Blanchette
2023 J jnl
Complete and Efficient Higher-Order Reasoning via Lambda-Superposition.
ACM SIGLOG News
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Uwe Waldmann
2023 — conf
Extending a High-Performance Prover to Higher-Order Logic.
TACAS (2)
Petar Vukmirovic, Jasmin Blanchette, Stephan Schulz
2023 — ed.
Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26 - 31, 2021.
CICM Workshops
Jasmin Blanchette, James H. Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Müller, Yasmine Sharoda, Claudio Sacerdoti Coen
2023 J jnl
Mechanical Mathematicians.
Commun. ACM
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2023 — conf
Recurrence-Driven Summations in Automated Deduction.
FroCoS
Visa Nummelin, Jasmin Blanchette, Sander R. Dahmen
2023 J jnl
SAT-Inspired Eliminations for Superposition.
ACM Trans. Comput. Log.
Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule
2023 J jnl
SAT-Inspired Higher-Order Eliminations.
Log. Methods Comput. Sci.
Jasmin Blanchette, Petar Vukmirovic
2023 J jnl
Superposition for Higher-Order Logic.
J. Autom. Reason.
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic
2023 J jnl
Unifying Splitting.
J. Autom. Reason.
Gabriel Ebner, Jasmin Blanchette, Sophie Tourret
2023 A conf
Verified Given Clause Procedures.
CADE
Jasmin Blanchette, Qi Qiu, Sophie Tourret
2022 J jnl
A Comprehensive Framework for Saturation Theorem Proving.
J. Autom. Reason.
Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
2022 A ed.
Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings
IJCAR
Jasmin Blanchette, Laura Kovács, Dirk Pattinson
2022 J jnl
Extending a brainiac prover to lambda-free higher-order logic.
Int. J. Softw. Tools Technol. Transf.
Petar Vukmirovic, Jasmin Blanchette, Simon Cruanes, Stephan Schulz
2022 J jnl
Making Higher-Order Superposition Work.
J. Autom. Reason.
Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
2022 J jnl
SAT-Inspired Higher-Order Eliminations.
CoRR
Jasmin Blanchette, Petar Vukmirovic
2022 B conf
Seventeen Provers Under the Hammer.
ITP
Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel
2021 A conf
A Unifying Splitting Framework.
CADE
Gabriel Ebner, Jasmin Blanchette, Sophie Tourret
2021 B conf
A modular Isabelle framework for verifying saturation provers.
CPP
Sophie Tourret, Jasmin Blanchette
2021 — conf
FMM Preface.
CICM Workshops
Jasmin Blanchette, Adam Naumowicz
2021 A conf
Making Higher-Order Superposition Work.
CADE
Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret
2021 J jnl
Message from the New Editor-in-Chief.
J. Autom. Reason.
Jasmin Blanchette
2021 B conf
SAT-Inspired Eliminations for Superposition.
FMCAD
Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule
2021 A conf
Superposition for Full Higher-order Logic.
CADE
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic
2021 J jnl
Superposition for Lambda-Free Higher-Order Logic.
Log. Methods Comput. Sci.
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
2021 J jnl
Superposition with Lambdas.
CoRR
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2021 J jnl
Superposition with Lambdas.
J. Autom. Reason.
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2020 — conf
A Comprehensive Framework for Saturation Theorem Proving.
IJCAR (1)
Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette
2020 J jnl
Extensions to the Comprehensive Framework for Saturation Theorem Proving.
Arch. Formal Proofs
Jasmin Blanchette, Sophie Tourret
2020 J jnl
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.
J. Autom. Reason.
Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann
2020 B ed.
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020.
CPP
Jasmin Blanchette, Catalin Hritcu
2020 J jnl
Superposition for Lambda-Free Higher-Order Logic.
CoRR
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann
2019 J jnl
Introduction to the STAF 2015 special section.
Softw. Syst. Model.
Jasmin Blanchette, Francis Bordeleau, Alfonso Pierantonio, Nikolai Kosmatov, Gabriele Taentzer, Manuel Wimmer
2019 A conf
Superposition with Lambdas.
CADE
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, Uwe Waldmann
2008 — book
C++ GUI Programming with Qt 4, 2nd Edition.
Jasmin Blanchette, Mark Summerfield