Florian Lonsing

Computer Scientist

Selected research projects:

My research covers the fields of automated reasoning, computational logic, and formal verification of hardware and software in broad sense. More specifically, in my research I focused on two interrelated areas: (1) automated reasoning approaches to solve quantified Boolean formulas (QBFs) and (2) theory and practice of hardware model checking and design verification.

Representative publications:

Self-Consistency Checking for Hardware Verification

I contributed to theoretical frameworks and mathematical proofs of formal guarantees of self-consistency checking for pre-silicon verification of hardware accelerator and processor designs.

Selected publications and resources:

Hardware Model Checking Based on Satisfiability Modulo Theories (SMT)

I contributed to the development of the SMT-based model checker Pono, written in C++, and also worked on performance profiling and tuning. We presented an in-depth performance study that highlighted the individual strengths of the different model checking engines implemented in Pono.

Selected publications and resources:

Usability, Robustness, and Performance of QBF Solving and Applications

I integrated incremental solving in the search-based solver DepQBF via a novel API. We demonstrated its effectiveness in several application case studies. Additionally, I co-authored QBF tool performance studies.

Selected publications and resources:

Parallel QBF Solving

I co-developed two orthogonal approaches to parallel QBF solving by search space splitting and portfolio, respectively. Additionally, I co-authored a related book chapter.

Selected publications and resources:

Improvements to Search-Based QBF Solving: Theory and Practice

I contributed to several improvements to QBF solving based on conflict-driven clause learning as implemented in the search-based solver DepQBF, e.g., by leveraging more powerful variants of resolution for clause learning. These variants result in a potentially exponential speed-up of solving time.

Selected publications and resources:

Improvements to QBF Preprocessing

We defined and implemented clause preprocessing techniques that improved the performance of state-of-the-art QBF solvers as shown in related studies.

Selected publications and resources:

PhD Project: Exploiting Variable Independence in Search-Based QBF Solving

I devised data structures and algorithms to efficiently exploit independent variables in search-based QBF solving based on a QBF-specific variant of the CDCL (conflict-driven clause learning) algorithm. In related work, it was shown that this approach potentially enables an exponential speed-up in solving time. I implemented it in a new QBF solver called DepQBF that achieved several top rankings in QBF solver competitions.

Selected publications and resources:

Fuzzing and Delta-Debugging for SAT and QBF Solvers

We developed tools to randomly test SAT and QBF solvers by fuzz testing and delta-debugging. In a case study using our tools, we detected previously unknown bugs in state-of-the-art SAT and QBF solvers.

Selected publications and resources:

QBF Proof Generation and Checking

As an approach to verify the correctness and robustness of QBF solvers, we presented efficient techniques and a related tool chain to extract and check QBF resolution proofs and to extract and check Skolem and Herbrand functions as models of satisfiable QBFs and countermodels of unsatisfiable QBFs, respectively.

Selected publications and resources:

Preprocessing QBFs

We devised and implemented a preprocessing approach to efficiently derive new unit clauses from a given QBF. Additionally, I contributed to a QBF clause elimination technique that lifts a known technique from SAT to the QBF level. These preprocessing approaches potentially enable an exponential speed-up in solving time.

Selected publications and resources:

MSc Project: QBF Solving by Quantifier Elimination

Nenofex (negation normal form expansion) is a solver for quantified boolean formulae (QBF) in negation normal form (NNF) that relies on expansion as the core technique for eliminating variables. Expansion is a QBF solving paradigm that is orthogonal to search-based solving using the conflict-driven clause learning (CDCL) approach.

Selected publications and resources: