default search action

combined dblp search
author search
venue search
publication search

ask others

Mathias Fleury

> Home > Persons

Person information

affiliation: University of Freiburg, Germany

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

2020 – today

see FAQ

What is the meaning of the colors in the publication lists?

2024
[c24]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/BiereFFFFP24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BiereFFFFP24
Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt:
CaDiCaL 2.0. CAV (1) 2024: 133-152
[c23]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/FazekasPFB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/FazekasPFB24
Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere:
Certifying Incremental SAT Solving. LPAR 2024: 321-340
[c22]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/sat/BiereFFF24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/BiereFFF24
Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks:
Clausal Congruence Closure. SAT 2024: 6:1-6:25
[c21]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/sat/CoutelierFK24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/CoutelierFK24
Robin Coutelier, Mathias Fleury, Laura Kovács:
Lazy Reimplication in Chronological Backtracking. SAT 2024: 9:1-9:19
[c20]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/LachnittFARBNBT24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/LachnittFARBNBT24
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) 2024: 311-330
[i2]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2402-01202
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2402-01202
Mathias Fleury, Daniela Kaufmann:
Life span of SAT techniques. CoRR abs/2402.01202 (2024)
2023
[c19]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/FleuryL23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/FleuryL23
Mathias Fleury, Peter Lammich:
A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper). CADE 2023: 207-219
[c18]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/sat/PollittFB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/PollittFB23
Florian Pollitt, Mathias Fleury, Armin Biere:
Faster LRAT Checking Than Solving with CaDiCaL. SAT 2023: 21:1-21:12
[c17]
- view
  - electronic edition @ ceur-ws.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/sat/BiereFFH23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/BiereFFH23
Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule:
The SAT Museum. POS@SAT 2023: 72-87
[c16]
- view
  - electronic edition @ ceur-ws.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/smt/LachnittFA0BNBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/LachnittFA0BNBT23
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT 2023: 78
2022
[j7]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/fmsd/FleuryB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/FleuryB22
Mathias Fleury, Armin Biere:
Mining definitions in Kissat with Kittens. Formal Methods Syst. Des. 60(3): 381-404 (2022)
[j6]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jair/CaiZFB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jair/CaiZFB22
Shaowei Cai, Xindi Zhang, Mathias Fleury, Armin Biere:
Better Decision Heuristics in CDCL through Local Search and Target Phases. J. Artif. Intell. Res. 74: 1515-1563 (2022)
[i1]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2207-13577
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2207-13577
Mathias Fleury, Armin Biere:
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses. CoRR abs/2207.13577 (2022)
2021
[c15]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cade/SchurrFD21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/SchurrFD21
Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais:
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. CADE 2021: 450-467
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/FleuryB21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/FleuryB21
Mathias Fleury, Armin Biere:
Efficient All-UIP Learned Clause Minimization. SAT 2021: 171-187
[c13]
- view
  - electronic edition @ ceur-ws.org (open access)
  - no references & citations available
- export record
  dblp key:
  - conf/smt/SchurrFD21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/SchurrFD21
Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais:
Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant. SMT 2021: 64
[c12]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2107-02354
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2107-02354
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine:
Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP 2021: 49-54
[e1]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2107-01544
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2107-01544
Chantal Keller, Mathias Fleury:
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021. EPTCS 336, 2021 [contents]
2020
[b1]
- view
  authority control:
- export record
  dblp key:
  - phd/dnb/Fleury20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/phd/dnb/Fleury20
Mathias Fleury:
Formalization of logical calculi in Isabelle/HOL. Saarland University, Saarbrücken, Germany, 2020
[j5]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/FleuryK20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/FleuryK20
Mathias Fleury, Daniela Kaufmann:
Practical Algebraic Calculus Checker. Arch. Formal Proofs 2020 (2020)
[j4]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BarbosaBFF20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BarbosaBFF20
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64(3): 485-510 (2020)
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/KaufmannFB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/KaufmannFB20
Daniela Kaufmann, Mathias Fleury, Armin Biere:
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus. FMCAD 2020: 264-269
[c10]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/FleuryW20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/FleuryW20
Mathias Fleury, Christoph Weidenbach:
A Verified SAT Solver Framework including Optimization and Partial Valuations. LPAR 2020: 212-229
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/HeisingerFB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/HeisingerFB20
Maximilian Heisinger, Mathias Fleury, Armin Biere:
Distributed Cube and Conquer with Paracooba. SAT 2020: 114-122

2010 – 2019

see FAQ

What is the meaning of the colors in the publication lists?

2019
[c8]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BrombergerFSW19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BrombergerFSW19
Martin Bromberger, Mathias Fleury, Simon Schwarz, Christoph Weidenbach:
SPASS-SATT - A CDCL(LA) Solver. CADE 2019: 111-122
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/nfm/Fleury19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nfm/Fleury19
Mathias Fleury:
Optimizing a Verified SAT Solver. NFM 2019: 148-165
[c6]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-1908-09480
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1908-09480
Mathias Fleury, Hans-Jörg Schurr:
Reconstructing veriT Proofs in Isabelle/HOL. PxTP 2019: 36-50
2018
[j3]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchetteFLW18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchetteFLW18
Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason. 61(1-4): 333-365 (2018)
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FleuryBL18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FleuryBL18
Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich:
A verified SAT solver with watched literals using imperative HOL. CPP 2018: 158-171
2017
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/frocos/BiendarraBBDFHK17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/frocos/BiendarraBBDFHK17
Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel:
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 2017: 3-21
[c3]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/ijcai/BlanchetteFW17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ijcai/BlanchetteFW17
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAI 2017: 4786-4790
[c2]
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/rta/BlanchetteFT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/rta/BlanchetteFT17
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. FSCD 2017: 11:1-11:18
2016
[j2]
- view
  - electronic edition @ isa-afp.org (open access)
  - no references & citations available
- export record
  dblp key:
  - journals/afp/BlanchetteFT16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BlanchetteFT16
Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. Arch. Formal Proofs 2016 (2016)
[j1]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BlanchetteBFSS16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BlanchetteBFSS16
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier:
Semi-intelligible Isar Proofs from Machine-Generated Proofs. J. Autom. Reason. 56(2): 155-200 (2016)
[c1]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BlanchetteFW16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BlanchetteFW16
Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach:
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. IJCAR 2016: 25-44

Coauthor Index

see FAQ

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.