Florian Lonsing
| e-mail: | "fml" followed by the at-sign and "florianlonsing.com" |
|---|---|
| WWW: | http://www.florianlonsing.com/ |
|
Florian Lonsing |
|||
|
|
||||
|
| Home | Publications | Software | Talks |
I am a former applied scientist (Amazon Web Services). My research interests are in automated reasoning and satisfiability solving.
From January 2019 to October 2022, I was a researcher in Clark Barrett's group in the Computer Science Department at Stanford University. 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).
Satisfiability solving (SAT, QBF; theory, applications), automated reasoning, artificial intelligence, formal verification, SMT-based model checking, computational logic.
Several prizes won in QBF competition tracks with QBF solver DepQBF and related tools, jointly with my co-authors.
Runner-up of the Heinz Zemanek Dissertation Award 2016 of the Austrian Computer Society.
Reward check from Donald Knuth for a comment on his book The Art of Computer Programming, Volume 4, Fascicle 6: "Satisfiability".
Winner of the 2019 IJCAI-JAIR Best Paper Prize for the paper Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. 53: 127-168 (2015), jointly with Marijn Heule, Matti Järvisalo, Martina Seidl, and Armin Biere.
Honorable Mention for our paper A Theoretical Framework for Symbolic Quick Error Detection at Formal Methods in Computer-Aided Design (FMCAD) 2020 conference, jointly with Clark Barrett and Subhasish Mitra.
Invited commentary on our paper Evaluating QBF Solvers: Quantifier Alternations Matter published at the International Conference on Principles and Practice of Constraint Programming (CP) 2018, on the occasion of the 25th edition of CP.
Winner of the Oski Award with the model checker CoSA2 (now called Pono) in the Hardware Model Checking Competition 2019, jointly with Makai Mann, Ahmed Irfan, and Clark Barrett.
Joint best student paper award at the Bit-Precise Reasoning Workshop 2008.
April 2021: invited tutorial on QBF solving, jointly with Martina Seidl, in the Beyond Satisfiability Workshop, part of the Satisfiability: Theory, Practice, and Beyond program at the Simons Institute.
September 2020: our paper A Theoretical Framework for Symbolic Quick Error Detection received an Honorable Mention at FMCAD 2020.
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.
Link to list of software.
Link to list of talks.