| 2022 | GI | Implementations for Shor's algorithm for the DLP. | Alexander Mandl, Uwe Egly |
| 2019 | SAT | QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. | Florian Lonsing, Uwe Egly |
| 2018 | CADE | QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. | Florian Lonsing, Uwe Egly |
| 2018 | CP | Evaluating QBF Solvers: Quantifier Alternations Matter. | Florian Lonsing, Uwe Egly |
| 2018 | FMCAD | Expansion-Based QBF Solving Without Recursion. | Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadzic, Uwe Egly, Florian Lonsing, Martina Seidl |
| 2017 | CADE | DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. | Florian Lonsing, Uwe Egly |
| 2016 | SAT | On Stronger Calculi for QBFs. | Uwe Egly |
| 2016 | SAT | Q-Resolution with Generalized Axioms. | Florian Lonsing, Uwe Egly, Martina Seidl |
| 2015 | LPAR | Automated Benchmarking of Incremental SAT and QBF Solvers. | Uwe Egly, Florian Lonsing, Johannes Oetsch |
| 2015 | LPAR | Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. | Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl |
| 2015 | SAT | Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. | Florian Lonsing, Uwe Egly |
| 2014 | AISC | Conformant Planning as a Case Study of Incremental QBF Solving. | Uwe Egly, Martin Kronegger, Florian Lonsing, Andreas Pfandler |
| 2014 | CP | Incremental QBF Solving. | Florian Lonsing, Uwe Egly |
| 2014 | FMCAD | SAT-based methods for circuit synthesis. | Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Knighofer, Florian Lonsing |
| 2013 | LPAR | Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. | Uwe Egly, Florian Lonsing, Magdalena Widl |
| 2013 | SAT | Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. | Florian Lonsing, Uwe Egly, Allen Van Gelder |
| 2012 | COMMA | Complexity of logic-based argumentation in Schaefer's framework. | Nadia Creignou, Uwe Egly, Johannes Schmidt |
| 2012 | SAT | On Sequent Systems and Resolution for QBFs. | Uwe Egly |
| 2012 | SLE | Guided Merging of Sequence Diagrams. | Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits |
| 2012 | TAP | Towards Scenario-Based Testing of UML Diagrams. | Petra Brosch, Uwe Egly, Sebastian Gabmeyer, Gerti Kappel, Martina Seidl, Hans Tompits, Magdalena Widl, Manuel Wimmer |
| 2012 | TAP | A Framework for the Specification of Random SAT and QSAT Formulas. | Nadia Creignou, Uwe Egly, Martina Seidl |
| 2011 | MODELS | Towards Semantics-Aware Merge Support in Optimistic Model Versioning. | Petra Brosch, Uwe Egly, Sebastian Gabmeyer, Gerti Kappel, Martina Seidl, Hans Tompits, Magdalena Widl, Manuel Wimmer |
| 2009 | SAT | (1, 2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms. | Nadia Creignou, Herv Daud, Uwe Egly, Raphal Rossignol |
| 2008 | ICLP | ASPARTIX: Implementing Argumentation Frameworks Using Answer-Set Programming. | Uwe Egly, Sarah Alice Gaggl, Stefan Woltran |
| 2008 | SAT | New Results on the Phase Transition for Random Quantified Boolean Formulas. | Nadia Creignou, Herv Daud, Uwe Egly, Raphal Rossignol |
| 2006 | COMMA | Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas. | Uwe Egly, Stefan Woltran |
| 2006 | ECAI | A Solver for QBFs in Nonprenex Form. | Uwe Egly, Martina Seidl, Stefan Woltran |
| 2003 | SAT | Comparing Different Prenexing Strategies for Quantified Boolean Formulas. | Uwe Egly, Martina Seidl, Hans Tompits, Stefan Woltran, Michael Zolda |
| 2002 | CADE | Embedding Lax Logic into Intuitionistic Logic. | Uwe Egly |
| 2001 | CADE | Deriving Modular Programs from Short Proofs. | Uwe Egly, Stephan Schmitt |
| 2000 | AAAI | Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. | Uwe Egly, Thomas Eiter, Hans Tompits, Stefan Woltran |
| 2000 | TABLEAUX | Properties of Embeddings from Int to S4. | Uwe Egly |
| 1998 | AISC | Intuitionistic Proof Transformations and Their Application to Constructive Program Synthesis. | Uwe Egly, Stephan Schmitt |
| 1998 | CSL | Quantifers and the System KE: Some Surprising Results. | Uwe Egly |
| 1998 | TABLEAUX | On Proof Complexity of Circumscription. | Uwe Egly, Hans Tompits |
| 1997 | CADE | Some Pitfalls of LK-to-LJ Translations and How to Avoid Them. | Uwe Egly |
| 1997 | ECSQARU | Non-elementary Speed-Ups in Default Reasoning. | Uwe Egly, Hans Tompits |
| 1997 | LPNMR | Is Non-Monotonic Reasoning Always Harder? | Uwe Egly, Hans Tompits |
| 1997 | TABLEAUX | Lean Induction Principles for Tableaux. | Matthias Baaz, Uwe Egly, Christian G. Fermller |
| 1997 | TABLEAUX | Non-elementary Speed-ups in Proof Length by Different Variants of Classical Analytic Calculi. | Uwe Egly |
| 1996 | CADE | On the Practical Value of Different Definitional Translations to Normal Form. | Uwe Egly, Thomas Rath |
| 1995 | EPIA | Super-Polynomial Speed-Ups in Proof Length by New Tautologies. | Uwe Egly |
| 1995 | TABLEAUX | Issues in Theorem Proving Based on the Connection Method. | Wolfgang Bibel, Stefan Brning, Uwe Egly, Daniel S. Korn, Thomas Rath |
| 1994 | CADE | KoMeT. | Wolfgang Bibel, Stefan Brning, Uwe Egly, Thomas Rath |
| 1994 | LPAR | On the Value of Antiprenexing. | Uwe Egly |
| 1993 | LPAR | A First Order Resolution Calculus with Symmetries. | Uwe Egly |
| 1992 | ECAI | A Simple Proof for the Pigeonhole Formulae. | Uwe Egly |
| 1992 | LPAR | Shortening Proofs by Quantifier Introduction. | Uwe Egly |