2024

Robin Coutelier, Mathias Fleury and Laura Kovács, Lazy Reimplication in Chronological Backtracking
SAT 2024 preprint 
@InProceedings{coutelier_et_al:LIPIcs.SAT.2024.9,
  author =	{Coutelier, Robin and Fleury, Mathias and Kov\'{a}cs, Laura},
  title =	{{Lazy Reimplication in Chronological Backtracking}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9},
  URN =		{urn:nbn:de:0030-drops-205313},
  doi =		{10.4230/LIPIcs.SAT.2024.9},
  annote =	{Keywords: Chronological Backtracking, CDCL, Invariants, Watcher Lists}
}

Armin Biere, Katalin Fazekas, Mathias Fleury and Nils Frolekys, Clausal Congruence Closure
SAT 2024 preprint 
@InProceedings{BiereFazekasFleuryFroleyks-SAT24,
  author =	{Biere, Armin and Fazekas, Katalin and Fleury, Mathias and Froleyks, Nils},
  title =	{{Clausal Congruence Closure}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.6},
  URN =		{urn:nbn:de:0030-drops-205287},
  doi =		{10.4230/LIPIcs.SAT.2024.6},
}

Armin Biere, Tobias Faller Katalin Fazekas, Mathias Fleury, Nils Froleyks and Florian Pollitt, CaDiCaL 2.0
CAV 2024 paper 
@inproceedings{BiereFallerFazekasFleuryFroleyks-CAV24,
  author       = {Armin Biere and
                  Tobias Faller and
                  Katalin Fazekas and
                  Mathias Fleury and
                  Nils Froleyks and
                  Florian Pollitt},
  editor       = {Arie Gurfinkel and
                  Vijay Ganesh},
  title        = {{CaDiCaL 2.0}},
  booktitle    = {Computer Aided Verification - 36th International Conference, {CAV}
                  2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part {I}},
  series       = {Lecture Notes in Computer Science},
  volume       = {14681},
  pages        = {133--152},
  publisher    = {Springer},
  year         = {2024},
  doi          = {10.1007/978-3-031-65627-9\_7},
}

Katalin Fazekas, Florian Pollitt, Mathias Fleury and Armin Biere, Certifying Incremental SAT Solving
LPAR 2024 paper 
@inprocessing{FazekasPollittFleuryBiere-LPAR24,
  author       = {Katalin Fazekas and
                  Florian Pollitt and
                  Mathias Fleury and
                  Armin Biere},
  editor       = {Nikolaj S. Bj{\o}rner and
                  Marijn Heule and
                  Andrei Voronkov},
  title        = {Certifying Incremental {SAT} Solving},
  booktitle    = {{LPAR} 2024: Proceedings of 25th Conference on Logic for Programming,
                  Artificial Intelligence and Reasoning, Port Louis, Mauritius, May
                  26-31, 2024},
  series       = {EPiC Series in Computing},
  volume       = {100},
  pages        = {321--340},
  publisher    = {EasyChair},
  year         = {2024},
  url          = {https://doi.org/10.29007/pdcc},
  doi          = {10.29007/PDCC},
}

Katalin Fazekas, Florian Pollitt, Mathias Fleury, and Armin Biere, Incremental Proofs for Bounded Model Checking.
MBMV'24 Preprint 
@inproceedings{FazekasPollittFleuryBiere-MBMV24,
  author       = {Katalin Fazekas and
                Florian Pollitt and
                Mathias Fleury and
                Armin Biere},
  editor       = {Wolfgang Kunz}
  title        = {Incremental Proofs for Bounded Model Checking},
  booktitle    = {27th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
                  (MBMV'24), Kaiserslautern, Germany},
  series       = {ITG-Fachberichte},
  volume       = {314},
  pages        = {133--143},
  publisher    = {VDE Verlag},
  year         = {2024},
}

Mathias Fleury and Daniela Kaufmann, Lifespan of SAT techniques
Arxiv version of POS 23 https://arxiv.org/abs/2402.01202 
@misc{fleury2024life,
      title={Life span of SAT techniques},
      author={Mathias Fleury and Daniela Kaufmann},
      year={2024},
      eprint={2402.01202},
      archivePrefix={arXiv},
      primaryClass={cs.LO}
}

2023

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Noetzli, Clark W. Barrett and Cesare Tinelli, Automatic Verification of {SMT} Rewrites in Isabelle/HOL
SMT Workshop 2023 Abstract 
@inproceedings{LachnittFleuryEtAlCVC5Rare,
  author       = {Hanna Lachnitt and
                  Mathias Fleury and
                  Leni Aniva and
                  Andrew Reynolds and
                  Haniel Barbosa and
                  Andres N{\"{o}}tzli and
                  Clark W. Barrett and
                  Cesare Tinelli},
  editor       = {St{\'{e}}phane Graham{-}Lengrand and
                  Mathias Preiner},
  title        = {Automatic Verification of {SMT} Rewrites in Isabelle/HOL},
  booktitle    = {Proceedings of the 21st International Workshop on Satisfiability Modulo
                  Theories {(SMT} 2023) co-located with the 29th International Conference
                  on Automated Deduction {(CADE} 2023), Rome, Italy, July, 5-6, 2023},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {3429},
  pages        = {78},
  publisher    = {CEUR-WS.org},
  year         = {2023},
  url          = {https://ceur-ws.org/Vol-3429/abstract14.pdf},
  timestamp    = {Wed, 05 Jul 2023 16:52:15 +0200},
  biburl       = {https://dblp.org/rec/conf/smt/LachnittFA0BNBT23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Armin Biere, Mathias Fleury, and Florian Pollitt, CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT Entering the SAT Competition 2023

SAT Competition 2023 system description
(not reviewed) 
@inproceedings{BiereFleuryPolitt-SAT-Competition-2023-solvers,
  author       = {Armin Biere and Mathias Fleury and Florian Pollitt},
  title	       = {{CaDiCaL\_vivinst}, {IsaSAT}, {Gimsatul}, {Kissat},
                  and {TabularaSAT} Entering the {SAT} Competition
                  2023},
  editor       = {Tomas Balyo and Nils Froleyks and Marijn Heule and
                  Markus Iser and Matti J{\"a}rvisalo and Martin Suda},
  booktitle    = {Proc.~of {SAT Competition} 2023 -- Solver and
                  Benchmark Descriptions},
  volume       = {B-2023-1},
  series       = {Department of Computer Science Report Series B},
  publisher    = {University of Helsinki},
  year	       = 2023,
  keywords     = {competition, cadical,kissat,isasat},
  pages	       = {14--15},
}

Robin Trüby, Mathias Fleury, and Armin Biere, Verifying Floating-Point Commutativity with GRS

SAT Competition 2023 benchmarks
(not reviewed) 
@inproceedings{TrubyFleuryBiere-SAT-Competition-2023-description,
  author       = {Robin Trüby and Mathias Fleury and Armin Biere},
  title	       = {Verifying Floating-Point Commutativity with {GRS}},
  editor       = {Tomas Balyo and Nils Froleyks and Marijn Heule and
                  Markus Iser and Matti J{\"a}rvisalo and Martin Suda},
  booktitle    = {Proc.~of {SAT Competition} 2023 -- Solver and
                  Benchmark Descriptions},
  volume       = {B-2023-1},
  series       = {Department of Computer Science Report Series B},
  publisher    = {University of Helsinki},
  year	       = 2023,
  keywords     = {competition},
  pages	       = {53},
}

Sonja Gurtner, Lucas Klemmer, Mathias Fleury and Daniel Große, Replacing RISC-V Instructions by Others

SAT Competition 2023 benchmarks
(not reviewed) 
@inproceedings{GurtnerKlemmerFleuryGrosse-SAT-Competition-2023-description,
  author       = {Sonja Gurtner and Lucas Klemmer and Mathias Fleury
                  and Daniel Große},
  title	       = {Replacing {RISC-V} Instructions by Others},
  editor       = {Tomas Balyo and Nils Froleyks and Marijn Heule and
                  Markus Iser and Matti J{\"a}rvisalo and Martin Suda},
  booktitle    = {Proc.~of {SAT Competition} 2023 -- Solver and
                  Benchmark Descriptions},
  volume       = {B-2023-1},
  series       = {Department of Computer Science Report Series B},
  publisher    = {University of Helsinki},
  year	       = 2023,
  keywords     = {competition},
  pages	       = {54},
}

Mathias Fleury and Peter Lammich, A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper)

CADE 29 Preprint Springer (OA, upcoming)
29th International Conference on
Automated Deduction 
upcoming

Florian Politt, Mathias Fleury, and Armin Biere, Faster LRAT Checking than Solving with CaDiCaL
SAT23 Preprint LiPiCS 
upcoming

Florian Politt, Mathias Fleury, and Armin Biere, Efficient Proof Checking with LRAT in CaDiCaL (work in progress)
MBMV 23 Preprint 
@inproceedings{lrat-mbmv,
  author       = {Florian Pollitt and Mathias Fleury and Armin Biere},
  title	       = {Efficient Proof Checking with LRAT in CaDiCaL (work
                  in progress)},
  editor       = {Armin Biere and Daniel Große},
  booktitle    = {24th {GMM/ITG/GI} Workshop on Methods and
                  Description Languages for Modelling and Verification
                  of Circuits and Systems, {MBMV} 2023, Freiburg,
                  Germany, March 23-23, 2023},
  year	       = 2023,
  publisher    = {{VDE}},
  pages	       = {64--67},
  note	       = {Accepted}
}

2022

Mathias Fleury and Armin Biere, Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses

POS 22 arXiV
Pragmatics of SAT 22 Accepted
(POS has no proceedings) 
@misc{FleuryBiere-POS22,
  title = {Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses},
  author = {Fleury, Mathias and Biere, Armin},
  editor = {Matti J\"arvisalo and Daniel Le Berre}
  doi = {10.48550/ARXIV.2207.13577},
  url = {https://arxiv.org/abs/2207.13577},
  publisher = {arXiv},
  year = {2022},
  note = {Pragmatics of SAT 22, POS'22}
}

Shaowei Cai, Xindi Zhang, Mathias Fleury, and Armin Biere, Better Decision Heuristics in CDCL through Local Search and Target Phases

FMSD JAIR
Accepted 
@article{DBLP:journals/jair/SubramanianTLC22,
  author    = {Shaowei Cai and Xindi Zhang and Mathias Fleury and Armin Biere},
  journal   = {J. Artif. Intell. Res.},
  title     = {Better Decision Heuristics in CDCL through Local Search and Target Phases},
  volume    = {74},
  pages     = {1515--1564},
  year      = {2022},
  note      = {Accepted},
  month     = {July},
}

Daniela Kaufmann, Mathias Fleury, Armin Biere, and Manuel Kauers Practical Algebraic Calculus and Nullstellensatz with the Checkers Pacheck and Pastèque and Nuss-Checker

FMSD Preprint
Accepted

2021

Mathias Fleury and Armin Biere, Efficient All-UIP Learned Clause Minimization

SAT'21, LNCS Preprint Springer
Proc. 24rd Intl. Conf. on Theory and
Applications of Satisfiability Testing

SAT'21, LNCS

@inproceedings{FleuryBiere-SAT19,
  author    = {Mathias Fleury and
               Armin Biere},
  editor    = {Chu Min Li and Felip Many\`a},
  title     = {Efficient All-UIP Learned Clause Minimization},
  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2021 - 24th
               International Conference, {SAT} 2021, Barcelona, Spain, July 5-9,
               2021, Proceedings},
  series    = {LNCS},
  publisher = {Springer},
  year      = {2021},
  note      = {to appear},
}

Mathias Fleury and Armin Biere, Efficient All-UIP Learned Clause Minimization (Extended Version)
Technical Report PDF JKU ePUB 
@techreport{FleuryBiere-FMV-TR-21-3,
  author =       {Mathias Fleury and Armin Biere},
  title =        {Efficient All-UIP Learned Clause Minimization (Extended
                  Version)},
  number =       {21/3},
  date =         {May 2021},
  institution =  {Johannes Kepler University Linz},
  address =      {FMV Reports Series, Institute for Formal Models and
                  Verification, Johannes Kepler University, Altenbergerstr. 69,
                  4040 Linz, Austria},
  year =         {2021},
  doi =          {10.350/fmvtr.2021-3},
  url =          {https://doi.org/10.350/fmvtr.2021-3},
}

Mathias Fleury, IsaSAT and Kissat entering the EDA Challenge 2021
Submitted to the EDA Challenge 2021 PDF

Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine Alethe: Towards a Generic SMT Proof Format (extended abstract)

PxTP'21 PDF EPTCS
Proof Exchange on
Theorem Proving 
@inproceedings{SchurrFleuryBarbosaFontaine-PxTP21,
  author    = {Schurr, Hans-J\"org and Fleury, Mathias and Barbosa, Haniel and Fontaine, Pascal},
  year      = {2021},
  title     = {Alethe: Towards a Generic SMT Proof Format (extended abstract)},
  editor    = {Keller, Chantal and Fleury, Mathias},
  booktitle = {{\rm Proceedings Seventh Workshop on}
               Proof eXchange for Theorem Proving,
               {\rm Pittsburg, USA, 11th July 2021}},
  series    = {Electronic Proceedings Ain Theoretical Computer Science},
  volume    = {336},
  publisher = {Open Publishing Association},
  pages     = {49-54},
  doi       = {10.4204/EPTCS.336.6},
}

Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais, Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant

CADE 28 Springer (Open Access)
28th International Conference on
Automated Deduction 
@inproceedings{SchurrFleuryDesharnais-CADE28,
  author    = {Hans{-}J{\"{o}}rg Schurr and
               Mathias Fleury and
               Martin Desharnais},
  editor    = {Andr{\'{e}} Platzer and
               Geoff Sutcliffe},
  title     = {Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant},
  booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on
               Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {12699},
  pages     = {450--467},
  publisher = {Springer},
  year      = {2021},
  doi       = {10.1007/978-3-030-79876-5\_26},
}

2020

Maximilian Heisinger, Mathias Fleury, and Armin Biere, Distributed Cube and Conquer with Paracooba

SAT'20, LNCS Preprint Springer
Proc. 23rd Intl. Conf. on Theory and
Applications of Satisfiability Testing 
@inproceedings{HeisingerFleuryBiere-SAT20,
  author    = {Maximilian Heisinger and
               Mathias Fleury and
               Armin Biere},
  title     = {Distributed Cube and Conquer with Paracooba},
  booktitle = {{SAT}},
  series    = {LNCS},
  volume    = {12178},
  pages     = {114--122},
  publisher = {Springer},
  year      = {2020}
}

Daniela Kaufmann, Mathias Fleury, and Armin Biere. The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus

FMCAD'20 Preprint IEEE
Proc. Intl. Conf. on Formal Methods
in Computer Aided Design 
@inproceedings{KaufmannFleuryBiere-FMCAD20,
  author    = {Daniela Kaufmann and
               Mathias Fleury and
               Armin Biere},
  editor    = {Ofer Strichman and Alexander Ivrii},
  title     = {The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus},
  booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2020.},
  pages     = {264--269},
  volume	  = {1},
  publisher = {{TU Vienna Academic Press}},
  year      = {2020}
}

Mathias Fleury and Daniela Kaufmann. Practical Algebraic Calculus Checker. Archive of Formal Proofs Formal Development

AFP AFP entry
Archive of Formal Proofs 
@article{FleuryKaufmann-AFP20,
  author    = {Mathias Fleury and
               Daniela Kaufmann},
  title     = {Practical Algebraic Calculus Checker},
  journal   = {Arch. Formal Proofs},
  volume    = {2020},
  year      = {2020},
  url       = {https://www.isa-afp.org/entries/PAC_Checker.html},
}

Mathias Fleury and Christoph Weidenbach. A Verified SAT Solver Framework including Optimization and Partial Valuations

LPAR-23 PDF EasyChair
23rd International Conference on Logic for Programming,
Artificial Intelligence and Reasoning, 
@inproceedings{FleuryWeidenbach-LPAR23,
  author    = {Mathias Fleury and Christoph Weidenbach},
  title     = {A Verified SAT Solver Framework including Optimization and Partial Valuations},
  booktitle = {LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  editor    = {Elvira Albert and Laura Kovacs},
  series    = {EPiC Series in Computing},
  volume    = {73},
  pages     = {212--229},
  year      = {2020},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {https://easychair.org/publications/paper/b7Cr},
  doi       = {10.29007/96wb}
}

Mathias Fleury, Formalization of Logical Calculi in Isabelle/HOL (PhD thesis)
PhD thesis PDF University of Saarland 
@phdthesis{Fleury20,
  author    = {Mathias Fleury},
  title     = {Formalization of logical calculi in Isabelle/HOL},
  school    = {Saarland University, Saarbr{\"{u}}cken, Germany},
  year      = {2020},
  url       = {https://tel.archives-ouvertes.fr/tel-02963301},
}

2019

Mathias Fleury. Optimizing a Verified SAT Solver

NFM-19 Preprint Springer
NASA Formal Methods -
11th International Symposium 
@inproceedings{Fleury-NFM19,
  author    = {Mathias Fleury},
  editor    = {Julia M. Badger and
               Kristin Yvonne Rozier},
  title     = {Optimizing a Verified {SAT} Solver},
  booktitle = {{NASA} Formal Methods - 11th International Symposium, {NFM} 2019,
               Houston, TX, USA, May 7-9, 2019, Proceedings},
  series    = {LNCS},
  volume    = {11460},
  pages     = {148--165},
  publisher = {Springer},
  year      = {2019},
  doi       = {10.1007/978-3-030-20652-9\_10},
}

Mathias Fleury and Hans-Jörg Schurr, Reconstructing veriT proofs in Isabelle/HOL.

PxTP 2019 Arxiv
Sixth Workshop on
Proof eXchange for Theorem Proving 
@inproceedings{FleurySchurr-PxTP19,
  author    = {Mathias Fleury and
               Hans{-}J{\"{o}}rg Schurr},
  editor    = {Giselle Reis and
               Haniel Barbosa},
  title     = {Reconstructing {veriT} Proofs in {Isabelle}/{HOL}},
  booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving,
               PxTP 2019, Natal, Brazil, August 26, 2019},
  series    = {{EPTCS}},
  volume    = {301},
  pages     = {36--50},
  year      = {2019},
  url       = {https://doi.org/10.4204/EPTCS.301.6},
  doi       = {10.4204/EPTCS.301.6},
}

Martin Bromberger, Mathias Fleury, Simon Schwarz, and Christoph Weidenbach, SPASS-SATT a CDCL(LA) Solver.

CADE 27 Springer HAL
27th International Conference on
Automated Deduction 
@inproceedings{BrombergerFleurySchwarzWeidenbach-CADE27,
  author    = {Martin Bromberger and
               Mathias Fleury and
               Simon Schwarz and
               Christoph Weidenbach},
  editor    = {Pascal Fontaine},
  title     = {{SPASS-SATT} {A} {CDCL(LA)} Solver},
  booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on
               Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
  series    = {{LNCS}},
  volume    = {11716},
  pages     = {111--122},
  publisher = {Springer},
  year      = {2019},
  doi       = {10.1007/978-3-030-29436-6\_7},
}

Haniel Barbosa, Jasmin Blanchette, Mathias Fleury, and Pascal Fontaine. Scalable fine-grained proofs for formula processing.

JAR 20 Springer HAL
Journal of Automated Reasonning 
@article{BarbosaBlanchetteFleuryFontaine-JAR18,
  author    = {Haniel Barbosa and
               Blanchette, Jasmin Christian and
               Mathias Fleury and
               Pascal Fontaine},
  title     = {Scalable Fine-Grained Proofs for Formula Processing},
  journal   = {J. Autom. Reason.},
  volume    = {64},
  number    = {3},
  pages     = {485--510},
  year      = {2020},
  doi       = {10.1007/s10817-018-09502-y},
}

2018

Jasmin Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart and incrementality

JAR 18 Springer (Open Access)
Journal of Automated Reasonning 
@article{BlanchetteFleuryLammichWeidenbach-JAR18,
  author    = {Blanchette, Jasmin Christian and
               Mathias Fleury and
               Peter Lammich and
               Christoph Weidenbach},
  title     = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and
               Incrementality},
  journal   = {J. Autom. Reason.},
  volume    = {61},
  number    = {1-4},
  pages     = {333--365},
  year      = {2018},
  doi       = {10.1007/s10817-018-9455-7}
}

Jasmin Blanchette, Mathias Fleury, and Peter Lammich. A Verified SAT Solver with Watched Literals Using Imperative HOL.

CPP 18 ACM Matryoshka
7th ACM SIGPLAN International Conference on
Certified Programs and Proofs 
@inproceedings{FleuryBlanchetteLammich-CPP18,
  author    = {Mathias Fleury and
               Blanchette, Jasmin Christian and
               Peter Lammich},
  editor    = {June Andronick and
               Amy P. Felty},
  title     = {A verified {SAT} solver with watched literals using imperative {HOL}},
  booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
               Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
               8-9, 2018},
  pages     = {158--171},
  publisher = {{ACM}},
  year      = {2018},
  doi       = {10.1145/3167080},
}

2017

Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart and incrementality.

@inproceedings{BlanchetteFleuryWeidenbach-IJCAI17,
  author    = {Blanchette, Jasmin Christian and
               Mathias Fleury and
               Christoph Weidenbach},
  editor    = {Carles Sierra},
  title     = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and
               Incrementality},
  booktitle = {Proceedings of the Twenty-Sixth International Joint Conference on
               Artificial Intelligence, {IJCAI} 2017, Melbourne, Australia, August
               19-25, 2017},
  pages     = {4786--4790},
  publisher = {ijcai.org},
  year      = {2017},
  url       = {https://doi.org/10.24963/ijcai.2017/667},
  doi       = {10.24963/ijcai.2017/667},
  timestamp = {Sat, 05 Sep 2020 18:07:14 +0200},
  biburl    = {https://dblp.org/rec/conf/ijcai/BlanchetteFW17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

Julian Biendarra, Jasmin 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. Foundational (co)datatypes and (co)recursion for higher-order logic.

FroCoS 2017 Springer Matryoshka
11th International Symposium on
Frontiers of Combining Systems 
@inproceedings{Blanchette-datatypes17,
  author    = {Julian Biendarra and
               Blanchette, Jasmin Christian and
               Aymeric Bouzy and
               Martin Desharnais and
               Mathias Fleury and
               Johannes H{\"{o}}lzl and
               Ondrej Kuncar and
               Andreas Lochbihler and
               Fabian Meier and
               Lorenz Panny and
               Andrei Popescu and
               Christian Sternagel and
               Ren{\'{e}} Thiemann and
               Dmitriy Traytel},
  editor    = {Clare Dixon and
               Marcelo Finger},
  title     = {Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic},
  booktitle = {Frontiers of Combining Systems - 11th International Symposium, FroCoS
               2017, Bras{\'{\i}}lia, Brazil, September 27-29, 2017, Proceedings},
  series    = {LNCS},
  volume    = {10483},
  pages     = {3--21},
  publisher = {Springer},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-66167-4\_1},
  doi       = {10.1007/978-3-319-66167-4\_1},
  timestamp = {Sun, 25 Oct 2020 22:43:11 +0100},
  biburl    = {https://dblp.org/rec/conf/frocos/BiendarraBBDFHK17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

Jasmin Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL

@inproceedings{BlanchetteFleuryTraytel-FSCD17,
  author    = {Blanchette, Jasmin Christian and
               Mathias Fleury and
               Dmitriy Traytel},
  editor    = {Dale Miller},
  title     = {Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in
               Isabelle/HOL},
  booktitle = {2nd International Conference on Formal Structures for Computation
               and Deduction, {FSCD} 2017, September 3-9, 2017, Oxford, {UK}},
  series    = {LIPIcs},
  volume    = {84},
  pages     = {11:1--11:18},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2017},
  url       = {https://doi.org/10.4230/LIPIcs.FSCD.2017.11},
  doi       = {10.4230/LIPIcs.FSCD.2017.11},
  timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
  biburl    = {https://dblp.org/rec/conf/rta/BlanchetteFT17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

2016

Jasmin Blanchette, Mathias Fleury, Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart and incrementality

@inproceedings{BlanchetteFleuryWeidenbach-JAR16,
  author    = {Blanchette, Jasmin Christian and
               Mathias Fleury and
               Christoph Weidenbach},
  editor    = {Nicola Olivetti and
               Ashish Tiwari},
  title     = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and
               Incrementality},
  booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  series    = {LNCS},
  volume    = {9706},
  pages     = {25--44},
  publisher = {Springer},
  year      = {2016},
  doi       = {10.1007/978-3-319-40229-1\_4},
}

Jasmin Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier. Semi-intelligible Isar Proofs from Machine-Generated Proofs.

@article{BlanchetteBohmeFleurySmolkaStechermeier-JAR16,
  author    = {Blanchette, Jasmin Christian and
               Sascha B{\"{o}}hme and
               Mathias Fleury and
               Steffen Juilf Smolka and
               Albert Steckermeier},
  title     = {Semi-intelligible Isar Proofs from Machine-Generated Proofs},
  journal   = {J. Autom. Reason.},
  volume    = {56},
  number    = {2},
  pages     = {155--200},
  year      = {2016},
  doi       = {10.1007/s10817-015-9335-3},
}