| 2021 | BMVC | Intrinsic Examples: Robust Fingerprinting of Deep Neural Networks. | Siyue Wang, Pu Zhao, Xiao Wang, Sang Chin, Thomas Wahl, Yunsi Fei, Qi Alfred Chen, Xue Lin |
| 2021 | CAV | Delay-Bounded Scheduling Without Delay! | Andrew Johnson, Thomas Wahl |
| 2020 | DAC | Reverse-Engineering Deep Neural Networks Using Floating-Point Timing Side-Channels. | Cheng Gongye, Yunsi Fei, Thomas Wahl |
| 2020 | ICCAD | New Passive and Active Attacks on Deep Neural Networks in Medical Applications. | Cheng Gongye, Hongjia Li, Xiang Zhang, Majid Sabbagh, Geng Yuan, Xue Lin, Thomas Wahl, Yunsi Fei |
| 2019 | CAV | Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers. | Peizun Liu, Thomas Wahl, Akash Lal |
| 2018 | ICCAD | SCADET: a side-channel attack detection tool for tracking prime+probe. | Majid Sabbagh, Yunsi Fei, Thomas Wahl, A. Adam Ding |
| 2018 | PLDI | CUBA: interprocedural Context-UnBounded Analysis of concurrent programs. | Peizun Liu, Thomas Wahl |
| 2017 | DATE | Algebraic fault analysis of SHA-3. | Pei Luo, Konstantinos Athanasiou, Yunsi Fei, Thomas Wahl |
| 2017 | ICCD | Compiler-Assisted Threshold Implementation against Power Analysis Attacks. | Pei Luo, Konstantinos Athanasiou, Liwei Zhang, Zhen Hang Jiang, Yunsi Fei, A. Adam Ding, Thomas Wahl |
| 2017 | SEFM | IJIT: An API for Boolean Program Analysis with Just-in-Time Translation. | Peizun Liu, Thomas Wahl |
| 2017 | VMCAI | Stabilizing Floating-Point Programs Using Provenance Analysis. | Yijia Gu, Thomas Wahl |
| 2016 | CADE | Unbounded-Thread Program Verification using Thread-State Equations. | Konstantinos Athanasiou, Peizun Liu, Thomas Wahl |
| 2016 | FMCAD | Integrating proxy theories and numeric model lifting for floating-point arithmetic. | Jaideep Ramachandran, Thomas Wahl |
| 2016 | ICFEM | Concolic Unbounded-Thread Reachability via Loop Summaries. | Peizun Liu, Thomas Wahl |
| 2015 | ARITH | An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. | Martin Brain, Cesare Tinelli, Philipp Rmmer, Thomas Wahl |
| 2015 | EuroPar | Behavioral Non-portability in Scientific Numeric Computing. | Yijia Gu, Thomas Wahl, Mahsa Bayati, Miriam Leeser |
| 2014 | CONCUR | Lost in Abstraction: Monotonicity in Multi-threaded Programs. | Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2014 | DATE | Make it real: Effective floating-point reasoning via exact arithmetic. | Miriam Leeser, Saoni Mukherjee, Jaideep Ramachandran, Thomas Wahl |
| 2014 | FMCAD | Infinite-state backward exploration of Boolean broadcast programs. | Peizun Liu, Thomas Wahl |
| 2013 | FMCAD | The FMCAD graduate student forum. | Thomas Wahl |
| 2012 | CONCUR | Efficient Coverability Analysis by Proof Minimization. | Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2012 | TACAS | satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). | Grard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl |
| 2011 | CAV | Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs. | Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2011 | CAV | Linear Completeness Thresholds for Bounded Model Checking. | Daniel Kroening, Jol Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell |
| 2011 | VMCAI | Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2010 | CADE | An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2010 | CADE | Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. | Angelo Brillout, Daniel Kroening, Philipp Rmmer, Thomas Wahl |
| 2010 | CAV | Dynamic Cutoff Detection in Parameterized Concurrent Programs. | Alexander Kaiser, Daniel Kroening, Thomas Wahl |
| 2010 | TACAS | Boom: Taking Boolean Program Model Checking One Step Further. | Grard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao |
| 2009 | CAV | Symbolic Counter Abstraction for Concurrent Software. | Grard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening |
| 2009 | DATE | Strengthening properties using abstraction refinement. | Mitra Purandare, Thomas Wahl, Daniel Kroening |
| 2009 | FMCAD | Mixed abstractions for floating-point arithmetic. | Angelo Brillout, Daniel Kroening, Thomas Wahl |
| 2009 | IROS | Biologically inspired compliant control of a monopod designed for highly dynamic applications. | Sebastian Blank, Thomas Wahl, Tobias Luksch, Karsten Berns |
| 2009 | SAT | Finding Lean Induced Cycles in Binary Hypercubes. | Yury Chebiryak, Thomas Wahl, Daniel Kroening, Leopold Haller |
| 2009 | VMCAI | Extending Symmetry Reduction by Exploiting System Architecture. | Richard J. Trefler, Thomas Wahl |
| 2008 | TACAS | SVISS: Symbolic Verification of Symmetric Systems. | Thomas Wahl, Nicolas Blanc, E. Allen Emerson |
| 2007 | CAV | Adaptive Symmetry Reduction. | Thomas Wahl |
| 2006 | ICFEM | Reducing Model Checking of the Few to the One. | E. Allen Emerson, Richard J. Trefler, Thomas Wahl |
| 2005 | TACAS | Dynamic Symmetry Reduction. | E. Allen Emerson, Thomas Wahl |