47 citations · 188 across the 18 of their papers we have counts for
18 papers
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Haoze Wu, Christopher Hahn, Florian Lonsing +3
We present Self-Driven Strategy Learning (), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems.…
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni +12
Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique wh…
Effective Pre-Silicon Verification of Processor Cores by Breaking the Bounds of Symbolic Quick Error Detection
Karthik Ganesan, Florian Lonsing, Srinivasa Shashank Nuthakki +6
We present a novel approach to pre-silicon verification of processor designs. The purpose of pre-silicon verification is to find logic bugs in a design at an early stage and thus a…
A Theoretical Framework for Symbolic Quick Error Detection
Florian Lonsing, Subhasish Mitra, Clark Barrett
Symbolic quick error detection (SQED) is a formal pre-silicon verification technique targeted at processor designs. It leverages bounded model checking (BMC) to check a design for…
QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties
Florian Lonsing, Uwe Egly
We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the QRAT proof system and its generalization QRAT+. These systems rely on strong…
Expansion-Based QBF Solving Without Recursion
Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic +3
In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional…