Jasmin Blanchette

Cited by

	All	Since 2018
Citations	4477	1971
h-index	32	25
i10-index	56	48

480

240

120

360

200520062007200820092010201120122013201420152016201720182019202020212022202334 30 55 54 114 150 189 242 288 271 301 308 384 349 477 358 376 357 43

Public access

View all

61 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Andrei PopescuUniversity of SheffieldVerified email at sheffield.ac.uk
Dmitriy TraytelUniversity of CopenhagenVerified email at di.ku.dk
Lawrence PaulsonUniversity of CambridgeVerified email at cam.ac.uk
Cezary KaliszykUniversity of InnsbruckVerified email at uibk.ac.at
Petar VukmirovicVrije Universiteit AmsterdamVerified email at vu.nl
Tobias NipkowProfessor of Computer Science, Technische Universität MünchenVerified email at in.tum.de
Mathias FleuryUniversity FreiburgVerified email at informatik.uni-freiburg.de
Josef UrbanDistinguished Researcher at Czech Technical University in PragueVerified email at cvut.cz
Anders SchlichtkrullAalborg University CopenhagenVerified email at cs.aau.dk
Andreas LochbihlerDigital Asset (Switzerland) GmbHVerified email at inf.ethz.ch
Pascal FontaineLORIA, INRIA, Université de Lorraine, Nancy, FranceVerified email at loria.fr
Daniel KuehlweinCapgeminiVerified email at cs.ru.nl
Johannes HölzlVerified email at in.tum.de
Nicholas SmallboneChalmers University of TechnologyVerified email at chalmers.se
Christoph WeidenbachProfessor of Computer Science, Max Planck Institute for Informatics, Saarland Informatics CampusVerified email at mpi-inf.mpg.de
Stephan SchulzProfessor of Computer Science, DHBW StuttgartVerified email at eprover.org
Peter LammichThe University of ManchesterVerified email at in.tum.de
Haniel BarbosaAssistant Professor of Computer Science at Universidade Federal de Minas GeraisVerified email at dcc.ufmg.br
Andrew ReynoldsUniversity of IowaVerified email at uiowa.edu
Simon RobillardUniversité de MontpellierVerified email at umontpellier.fr

Jasmin Blanchette

Vrije Universiteit Amsterdam

Verified email at vu.nl - Homepage

Interactive and automatic theorem proving


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
C++ GUI Programming with Qt 4 J Blanchette, M Summerfield Pearson Education, 2008	1273*	2008
Nitpick: A counterexample generator for higher-order logic based on a relational model finder JC Blanchette, T Nipkow Interactive Theorem Proving: First International Conference, ITP 2010 …, 2010	309	2010
Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers LC Paulson, JC Blanchette IWIL @ LPAR, 2010	307	2010
Extending Sledgehammer with SMT solvers JC Blanchette, S Böhme, LC Paulson Journal of automated reasoning 51 (1), 109-128, 2013	283	2013
Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016	185	2016
Automatic proof and disproof in Isabelle/HOL JC Blanchette, L Bulwahn, T Nipkow Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011 …, 2011	125	2011
Truly modular (co)datatypes for Isabelle/HOL JC Blanchette, J Hölzl, A Lochbihler, L Panny, A Popescu, D Traytel Interactive Theorem Proving, 93-110, 2014	116	2014
MaSh: Machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban International Conference on Interactive Theorem Proving, 35-50, 2013	96	2013
Encoding monomorphic and polymorphic types JC Blanchette, S Böhme, A Popescu, N Smallbone Logical Methods in Computer Science 12, 2017	92*	2017
TFF1: The TPTP typed first-order form with rank-1 polymorphism JC Blanchette, A Paskevich Automated Deduction–CADE-24: 24th International Conference on Automated …, 2013	75	2013
Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving D Traytel, A Popescu, JC Blanchette Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer …, 2012	75	2012
A verified SAT solver framework with learn, forget, restart, and incrementality JC Blanchette, M Fleury, P Lammich, C Weidenbach Journal of automated reasoning 61, 333-365, 2018	69	2018
A learning-based fact selector for Isabelle/HOL JC Blanchette, D Greenaway, C Kaliszyk, D Kühlwein, J Urban Journal of Automated Reasoning 57, 219-244, 2016	64	2016
Mining the Archive of Formal Proofs JC Blanchette, M Haslbeck, D Matichuk, T Nipkow Intelligent Computer Mathematics, 3-17, 2015	56	2015
Superposition for lambda-free higher-order logic U Waldmann, S Cruanes, J Blanchette, A Bentkamp Logical Methods in Computer Science 17, 2021	50	2021
More SPASS with Isabelle: Superposition with hard sorts and configurable simplification JC Blanchette, A Popescu, D Wand, C Weidenbach Interactive Theorem Proving, 345-360, 2012	49	2012
A decision procedure for (co)datatypes in SMT solvers A Reynolds, JC Blanchette Automated Deduction-CADE-25, 197-213, 2015	48	2015
Superposition with lambdas A Bentkamp, J Blanchette, S Tourret, P Vukmirović, U Waldmann Journal of Automated Reasoning 65 (7), 893-940, 2021	44	2021
The Little Manual of API Design J Blanchette Trolltech, Nokia, 2008	44	2008
Extending a brainiac prover to lambda-free higher-order logic P Vukmirović, JC Blanchette, S Cruanes, S Schulz International Conference on Tools and Algorithms for the Construction and …, 2019	41	2019

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Follow

Cited by

Co-authors