[1] | Pei Luo, Konstantinos Athanasiou, Thomas Wahl, and Yunsi Fei (to appear). Algebraic fault analysis of SHA-3. In Design Automation and Test in Europe (DATE), 2017. [ bib ] |
[2] | Yijia Gu and Thomas Wahl. Stabilizing floating-point programs using provenance analysis (to appear). In Verification, Model Checking, and Abstraction Interpretation (VMCAI), 2017. [ bib ] |
[3] | 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 ] |
[4] | 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 ] |
[5] | 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 ] |
[6] | 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 ] |
[7] | 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 ] |
[8] | 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 ] |
[9] | 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 ] |
[10] | 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 ] |
[11] | Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Efficient coverability analysis by proof minimization. In Concurrency Theory (CONCUR), pages 500--515, 2012. [ bib | .pdf ] |
[12] | 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 ] |
[13] | 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 (ERTS^{2}), 2012. [ bib | .pdf ] |
[14] | 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 ] |
[15] | 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 ] |
[16] | Angelo Brillout, Daniel Kroening, Philipp Ruemmer, and Thomas Wahl. Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In Verification, Model Checking, and Abstraction Interpretation (VMCAI), pages 88--102, 2011. [ bib | .pdf ] |
[17] | 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 ] |
[18] | 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 ] |
[19] | 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 ] |
[20] | 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 ] |
[21] | 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 ] |
[22] | 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 ] |
[23] | 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 ] |
[24] | 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 ] |
[25] | 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 ] |
[26] | Thomas Wahl. Adaptive symmetry reduction. In Computer Aided Verification (CAV), pages 393--405, 2007. [ bib | .pdf ] |
[27] | 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 ] |
[28] | 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 ] |
[29] | 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 ] |
[30] | Oliver Karch, Hartmut Noltemeier, and Thomas Wahl. Robot localization using polygon distances. In Sensor Based Intelligent Robots, pages 200--219, 1998. [ bib | .pdf ] |
[31] | 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.98.