I am a researcher in Clark Barrett's group in the Computer Science Department at Stanford University, which I joined in January 2019. My position is part of the POSH Upscale project, which has the goal to develop tools and techniques for verifying and evaluating open-source hardware.
From June 2012 to September 2018 I was a postdoctoral researcher in the Knowledge-Based Systems Group (KBS) within the Institute of Logic and Computation at TU Wien, Austria. My position was part of the RiSE national research network.
Previously, from 2008 to 2012, I was assistant and doctoral student at the Institute of Formal Models and Verification (FMV) at Johannes Kepler University (JKU) in Linz, Austria.
Between 2008 and 2018, primarily I worked on solving techniques for quantified boolean formulae (QBF) and related practical aspects.
Since 2009, I have been developing the QBF solver DepQBF. See also my dissertation.
The latest release of DepQBF is available from GitHub: http://lonsing.github.io/depqbf/.
April 2018: first release of our new QBF preprocessor QRATPre+ (source code on GitHub, related paper at IJCAR 2018).
September 2019: on the occasion of the 25th Anniversary of the International Conference on Principles and Practice of Constraint Programming, we were invited to contribute a commentary on our CP 2018 paper (preprint). Our commentary (click here) appeared in a virtual CP Anniversary Volume organized by Gene Freuder. The volume contains commentaries on 25 papers, where one paper was chosen from each year of the CP conference since 1995.
August 2019: our JAIR article Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere: Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. 53: 127-168 (2015) was selected as the winner of the 2019 IJCAI-JAIR Best Paper Prize. The annual prize is awarded to an outstanding paper published in JAIR in the preceding five calendar years.
I was a co-organizer / program co-chair of:
Link to list of software.
Link to list of talks.