DI Florian Lonsing

From 2008 to 2012, I was doctoral student and assistant at FMV. In June 2012, I joined the Knowledge-Based Systems Group at Vienna University of Technology as a post-doctoral researcher.

My thesis (advisor: Armin Biere) can be found here: PDF.

By June 2012 this page is no longer maintained. My new webpage is at http://www.kr.tuwien.ac.at/staff/lonsing/.

Research Interests

QBF (Quantified Boolean Formulae)
SAT
Formal Verification

Publications

A list of my publications can be found here: Publications

Talk Slides

Blocked Clause Elimination for QBF, CADE'11, Wroclaw, Poland
Failed Literal Detection for QBF, SAT'11, Ann Arbor, Michigan, USA
Preprocessing QBF: Failed Literals and Quantified Blocked Clause Elimination , Deduction at Scale Seminar, Ringberg Castle, Tegernsee, Germany
Practical Aspects of Dependency Schemes in QBF Solving, AVM'10, Lugano, Switzerland
Integrating Dependency Schemes in Search-Based QBF Solvers ( Talk) ( Poster), SAT'10, Edinburgh, Scotland, UK
DepQBF: A Dependency-Aware QBF Solver (System Description), POS'10, Edinburgh, Scotland, UK
A Compact Representation for Syntactic Dependencies in QBFs, SAT'09, Swansea, Wales, UK
Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers, MEMICS'08, Znojmo, Czech Republic
Nenofex: Expanding NNF for QBF Solving, SAT'08, Guangzhou, P. R. China

Software

DepQBF, a search-based QBF solver.
QxBF, a QBF preprocessor based on failed literal detection.
BlocksQBF, a random QBF generator.
You might also be interested in QBFuzz, QBFDD, and Bloqqer.
Experimental tool on compact representations for dependencies in QBFs.

Teaching Activities

Formal Models (Formale Modelle), Exercises: Summer 2008, 2009, 2010, 2011
Spezielle Kapitel aus Informatik (Pthreads Programming in C): Summer 2008, 2009
Model Checking, Exercises: Winter 2008, 2009, 2010
Seminar in Formal Verification: Winter 2008, 2009

Awards

Best Student BPR Paper Award (sponsored by Fortify Software), R. Brummayer, A. Biere and F. Lonsing. BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking, BPR'08, Princeton, New Jersey, USA, July 2008.

Office

TNF Tower, 7th Floor, North-West Wing
+43 732 2468 8870 (phone)
Room T0762

Contact

https://fmv.jku.at/lonsing
+43 732 2468 8893 (fax)

Address

Institute for Formal Models and Verification
Johannes Kepler University
Altenbergerstr. 69
4040 Linz
Austria