| [1] | Andrew Johnson and Thomas Wahl. Delay-bounded scheduling without delay! In Computer Aided Verification (CAV), 2021. [ bib | .pdf ] |
| [2] | Cheng Gongye, Hongjia Li, Xiang Zhang, Majid Sabbagh, Geng Yuan, Xue Lin, Thomas Wahl, and Yunsi Fei. New passive and active attacks on deep neural networks in medical applications. In International Conference On Computer Aided Design (ICCAD), 2020. [ bib | .pdf ] |
| [3] | Konstantinos Athanasiou, Thomas Wahl, Adam Ding, and Yunsi Fei. Automatic detection and repair of transition- based leakage in software binaries. In Software Verification - 12th International Conference (VSTTE), 2020. [ bib | .pdf ] |
| [4] | Cheng Gongye, Yunsi Fei, and Thomas Wahl. Reverse engineering deep neural networks using floating-point timing side-channel. In Design Automation Conference (DAC), 2020. [ bib | .pdf ] |
| [5] | Peizun Liu, Thomas Wahl, and Akash Lal. Verifying asynchronous event-driven programs using partial abstract transformers. In Computer Aided Verification (CAV), pages 386--404, 2019. [ bib | .pdf ] |
| [6] | Majid Sabbagh, Yunsi Fei, Thomas Wahl, and Adam Ding. SCADET: A side-channel attack detection tool for tracking Prime+Probe. In International Conference on Computer-Aided Design (ICCAD), pages 107:1--107:8, 2018. [ bib | .pdf ] |
| [7] | Peizun Liu and Thomas Wahl. CUBA: Interprocedural context-unbounded analysis of concurrent programs. In Programming Languages Design and Implementation (PLDI), pages 105--119, 2018. [ bib | .pdf ] |
| [8] | Pei Luo, Konstantinos Athanasiou, Liwei Zhang, Zhen Hang Jiang, Yunsi Fei, Adam Ding, and Thomas Wahl. Compiler-assisted threshold implementation against power analysis attacks. In International Conference on Computer Design (ICCD), pages 541--544, 2017. [ bib | .pdf ] |
| [9] | Peizun Liu and Thomas Wahl. IJIT: An API for Boolean program analysis with just-in-time translation. In Software Engineering and Formal Methods (SEFM), pages 316--331, 2017. [ bib | .pdf ] |
| [10] | Pei Luo, Konstantinos Athanasiou, Yunsi Fei, and Thomas Wahl. Algebraic fault analysis of SHA-3. In Design Automation and Test in Europe (DATE), pages 151--156, 2017. [ bib | .pdf ] |
| [11] | Yijia Gu and Thomas Wahl. Stabilizing floating-point programs using provenance analysis. In Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 228--245, 2017. [ bib | .pdf ] |
| [12] | Peizun Liu and Thomas Wahl. Concolic unbounded-thread reachability via loop summaries. In International Conference on Formal Engineering Methods (ICFEM), pages 346--362, 2016. [ bib | .pdf ] |
| [13] | Jaideep Ramachandran and Thomas Wahl. Integrating proxy theories and numeric model lifting for floating-point arithmetic. In Formal Methods in Computer-Aided Design (FMCAD), pages 153--160, 2016. [ bib | .pdf ] |
| [14] | Konstantinos Athanasiou, Peizun Liu, and Thomas Wahl. Unbounded-thread program verification using thread-state equations. In International Joint Conference on Automated Reasoning (IJCAR), pages 516--531, 2016. [ bib | .pdf ] |
| [15] | Yijia Gu, Thomas Wahl, Mahsa Bayati, and Miriam Leeser. Behavioral non-portability in scientific numeric computing. In Parallel and Distributed Computing (EURO-PAR), pages 558--569, 2015. [ bib | .pdf ] |
| [16] | Martin Brain, Cesare Tinelli, Philipp Rümmer, and Thomas Wahl. An automatable formal semantics for IEEE-754 floating-point arithmetic. In Symposium on Computer Arithmetic (ARITH), pages 160--167, 2015. [ bib | .pdf ] |
| [17] | Peizun Liu and Thomas Wahl. Infinite-state backward exploration of Boolean broadcast programs. In Formal Methods in Computer-Aided Design (FMCAD), pages 155--162, 2014. [ bib | .pdf ] |
| [18] | Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Lost in abstraction: Monotonicity in multi-threaded programs. In Concurrency Theory (CONCUR), pages 141--155, 2014. [ bib | .pdf ] |
| [19] | Miriam Leeser, Saoni Mukherjee, Jaideep Ramachandran, and Thomas Wahl. Make it real: Effective floating-point reasoning via exact arithmetic. In Design Automation and Test in Europe (DATE), pages 1--4, 2014. [ bib | .pdf ] |
| [20] | Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Efficient coverability analysis by proof minimization. In Concurrency Theory (CONCUR), pages 500--515, 2012. [ bib | .pdf ] |
| [21] | Gérard Basler, Alastair Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl. SATABS: A bit-precise verifier for C programs (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 552--555, 2012. [ bib | .pdf ] |
| [22] | Nannan He, Daniel Kroening, Thomas Wahl, Kung-Kiu Lau, Faris Taweel, Tran Cuong, Philipp Ruemmer, and Sanjiv Sharma. Component-based design and verification in X-MAN. In Embedded Real Time Software and Systems (ERTS2), 2012. [ bib | .pdf ] |
| [23] | Daniel Kroening, Joel Ouaknine, Ofer Strichman, Thomas Wahl, and James Worrell. Linear completeness thresholds for bounded model checking. In Computer Aided Verification (CAV), pages 557--572, 2011. [ bib | .pdf ] |
| [24] | Alastair Donaldson, Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In Computer Aided Verification (CAV), pages 356--371, 2011. [ bib | .pdf ] |
| [25] | Angelo Brillout, Daniel Kroening, Philipp Ruemmer, and Thomas Wahl. Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 88--102, 2011. [ bib | .pdf ] |
| [26] | Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In Computer Aided Verification (CAV), pages 645--659, 2010. [ bib | .pdf ] |
| [27] | Angelo Brillout, Daniel Kroening, Philipp Ruemmer, and Thomas Wahl. An interpolating sequent calculus for quantier-free Presburger arithmetic. In International Joint Conference on Automated Reasoning (IJCAR), pages 384--399, 2010. [ bib | .pdf ] |
| [28] | Gerard Basler, Matthew Hague, Daniel Kroening, Luke Ong, Thomas Wahl, and Haoxian Zhao. Boom: Taking Boolean program model checking one step further. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 145--149, 2010. [ bib | .pdf ] |
| [29] | Angelo Brillout, Daniel Kroening, and Thomas Wahl. Mixed abstractions for floating-point arithmetic. In Formal Methods in Computer-Aided Design (FMCAD), pages 69--76, 2009. [ bib | .pdf ] |
| [30] | Gerard Basler, Michele Mazzucchi, Thomas Wahl, and Daniel Kroening. Symbolic counter abstraction for concurrent software. In Computer Aided Verification (CAV), pages 64--78, 2009. [ bib | .pdf ] |
| [31] | Yury Chebiryak, Thomas Wahl, Daniel Kroening, and Leopold Haller. A propositional encoding of lean induced cycles in binary hypercubes. In Theory and Applications of Satisfiability Testing (SAT), pages 18--31, 2009. [ bib | .pdf ] |
| [32] | Mitra Purandare, Daniel Kroening, and Thomas Wahl. Strengthening properties using abstraction refinement. In Design, Automation and Test in Europe (DATE), pages 1692--1697, 2009. [ bib | .pdf ] |
| [33] | Richard Trefler and Thomas Wahl. Extending symmetry reduction by exploiting system architecture. In Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 320--334, 2009. [ bib | .pdf ] |
| [34] | Thomas Wahl, Nicolas Blanc, and Allen Emerson. Sviss: Symbolic verification of symmetric systems. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 459--462, 2008. [ bib | .pdf ] |
| [35] | Thomas Wahl. Adaptive symmetry reduction. In Computer Aided Verification (CAV), pages 393--405, 2007. [ bib | .pdf ] |
| [36] | Allen Emerson, Richard Trefler, and Thomas Wahl. Reducing model checking of the few to the one. In International Conference on Formal Engineering Methods (ICFEM), pages 94--113, 2006. [ bib | .pdf ] |
| [37] | Allen Emerson and Thomas Wahl. Dynamic symmetry reduction. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 382--396, 2005. [ bib | .pdf ] |
| [38] | Allen Emerson and Thomas Wahl. On combining symmetry reduction and symbolic representation for efficient model checking. In Correct Hardware Design and Verification Methods (CHARME), pages 216--230, 2003. [ bib | .pdf ] |
| [39] | Oliver Karch, Hartmut Noltemeier, and Thomas Wahl. Robot localization using polygon distances. In Sensor Based Intelligent Robots, pages 200--219, 1998. [ bib | .pdf ] |
| [40] | Oliver Karch, Hartmut Noltemeier, Mathias Schwark, and Thomas Wahl. Relokalisation -- ein theoretischer Ansatz in der Praxis. In Autonomous Mobile Systems (AMS), pages 119--130, 1997. [ bib | .pdf ] |
This file was generated by bibtex2html 1.99.