| Mathematizing C++ concurrency M Batty, S Owens, S Sarkar, P Sewell, T Weber ACM SIGPLAN Notices 46 (1), 55-66, 2011 | 495 | 2011 |
| Fast LCF-style proof reconstruction for Z3 S Böhme, T Weber Interactive Theorem Proving: First International Conference, ITP 2010 …, 2010 | 169 | 2010 |
| A SAT-based Sudoku solver T Weber LPAR, 11-15, 2005 | 73 | 2005 |
| The SMT Competition 2015–2018 T Weber, S Conchon, D Déharbe, M Heizmann, A Niemetz, G Reger Journal on Satisfiability, Boolean Modeling and Computation 11 (1), 221-259, 2019 | 72 | 2019 |
| Efficiently checking propositional refutations in HOL theorem provers T Weber, H Amjad Journal of Applied Logic 7 (1), 26-40, 2009 | 72 | 2009 |
| The 2014 SMT competition DR Cok, D Déharbe, T Weber Journal on Satisfiability, Boolean Modeling and Computation 9 (1), 207-242, 2014 | 66 | 2014 |
| Towards mechanized program verification with separation logic T Weber International Workshop on Computer Science Logic, 250-264, 2004 | 65 | 2004 |
| Sat-based finite model generation for higher-order logic T Weber Technische Universität München, 2008 | 52 | 2008 |
| TOOLympics 2019: An overview of competitions in formal methods E Bartocci, D Beyer, PE Black, G Fedyukovich, H Garavel, A Hartmanns, ... Tools and Algorithms for the Construction and Analysis of Systems: 25 Years …, 2019 | 50 | 2019 |
| Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL S Böhme, ACJ Fox, T Sewell, T Weber Certified Programs and Proofs: First International Conference, CPP 2011 …, 2011 | 47 | 2011 |
| SMT solvers: New oracles for the HOL theorem prover T Weber International Journal on Software Tools for Technology Transfer 13 (5), 419-429, 2011 | 39 | 2011 |
| Nitpicking C++ concurrency JC Blanchette, T Weber, M Batty, S Owens, S Sarkar Proceedings of the 13th international ACM SIGPLAN symposium on Principles …, 2011 | 39 | 2011 |
| Kleene algebra A Armstrong, G Struth, T Weber Archive of Formal Proofs 324, 2013 | 38 | 2013 |
| Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL: (Invited Tutorial) S Foster, G Struth, T Weber Relational and Algebraic Methods in Computer Science: 12th International …, 2011 | 38 | 2011 |
| Towards automated proof support for probabilistic distributed systems AK McIver, T Weber International Conference on Logic for Programming Artificial Intelligence …, 2005 | 37 | 2005 |
| Modal logics for nominal transition systems J Parrow, J Borgström, LH Eriksson, RF Gutkovas, T Weber Logical Methods in Computer Science 17, 2021 | 32 | 2021 |
| Automating algebraic methods in Isabelle W Guttmann, G Struth, T Weber International Conference on Formal Engineering Methods, 617-632, 2011 | 30 | 2011 |
| Formal memory models for the verification of low-level operating-system code H Tews, M Völp, T Weber Journal of Automated Reasoning 42, 189-227, 2009 | 29 | 2009 |
| The 2013 evaluation of smt-comp and smt-lib DR Cok, A Stump, T Weber Journal of Automated Reasoning 55, 61-90, 2015 | 27 | 2015 |
| Integrating a SAT solver with an LCF-style theorem prover T Weber Electronic Notes in Theoretical Computer Science 144 (2), 67-78, 2006 | 26 | 2006 |
Georg StruthUniversity of SheffieldVerified email at sheffield.ac.uk
