Chair of Computer Architecture

This webpage is also available as long version with the bibtex entries (both pages are under construction).

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

• 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)

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

SAT Competition 2023	benchmarks
(not reviewed)

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

SAT Competition 2023 benchmarks
(not reviewed)

• 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

• Florian Politt, Mathias Fleury, and Armin Biere, Efficient Proof Checking with LRAT in CaDiCaL (work in progress)

MBMV 23	Preprint

• Florian Politt, Mathias Fleury, and Armin Biere, Faster LRAT Checking than Solving with CaDiCaL

SAT23	Preprint	LiPiCS

• Mathias Fleury and Daniela Kaufmann, Lifespan of SAT techniques

POS 23
Pragmatics of SAT 23	Accepted
	(POS has no proceedings)

• Armin Biere , Mathias Fleury , Nils Froleyks and Marijn Heule . The SAT Museum

POS 23
Pragmatics of SAT 23	Accepted
	(POS has no proceedings)

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)

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

FMSD	JAIR
Accepted

• 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	Springer
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

• Mathias Fleury and Armin Biere, Efficient All-UIP Learned Clause Minimization (Extended Version)

Technical Report	PDF	JKU ePUB

• 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

• 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

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

• 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

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

AFP	AFP entry
Archive of Formal Proofs

• 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,

• Mathias Fleury, Formalization of Logical Calculi in Isabelle/HOL (PhD thesis)

PhD thesis	PDF	University of Saarland

2019

• Mathias Fleury. Optimizing a Verified SAT Solver

NFM-19	Preprint	Springer
NASA Formal Methods -
11th International Symposium

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

PxTP 2019		Arxiv
Sixth Workshop on
Proof eXchange for Theorem Proving

• 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

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

JAR 20	Springer	HAL
Journal of Automated Reasonning

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

• 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

2017

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

IJCAI 17	IJCAI
Twenty-Sixth International Joint Conference on
Artificial Intelligence

• 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	ACM	Matryoshka
11th International Symposium on
Frontiers of Combining Systems

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

2016

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

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