Constructively Characterizing Fold and Unfold. - Tjark Weber; James L. Caldwell (LOPSTR, 2003)

Towards Mechanized Program Verification with Separation Logic. - Tjark Weber (CSL, 2004)

Bounded Model Generation for Isabelle/HOL. - Tjark Weber (D/PDPAR@IJCAR, 2004)

Towards Automated Proof Support for Probabilistic Distributed Systems. - Annabelle McIver; Tjark Weber (LPAR, 2005)

Integrating a SAT Solver with an LCF-style Theorem Prover. - Tjark Weber (PDPAR@CAV, 2005)

A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code. - Hendrik Tews; Tjark Weber; Marcus Völp (SSV, 2008)

SAT-based finite model generation for higher-order logic. - Tjark Weber (2008)

Finite Models in FOL-Based Crypto-Protocol Verification. - Jan Jürjens; Tjark Weber (ARSPA-WITS, 2009)

Efficiently checking propositional refutations in HOL theorem provers. - Tjark Weber; Hasan Amjad (J. Appl. Log., 2009)

Formal Memory Models for the Verification of Low-Level Operating-System Code. - Hendrik Tews; Marcus Völp; Tjark Weber (J. Autom. Reason., 2009)

Fast LCF-Style Proof Reconstruction for Z3. - Sascha Böhme; Tjark Weber (ITP, 2010)

Validating QBF Invalidity in HOL4. - Tjark Weber (ITP, 2010)

Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL - (Invited Tutorial). - Simon Foster 001; Georg Struth; Tjark Weber (RAMiCS, 2011)

A Repository for Tarski-Kleene Algebras. - Walter Guttmann; Georg Struth; Tjark Weber (ATE, 2011)

Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. - Sascha Böhme; Anthony C. J. Fox; Thomas Sewell; Tjark Weber (CPP, 2011)

Automating Algebraic Methods in Isabelle. - Walter Guttmann; Georg Struth; Tjark Weber (ICFEM, 2011)

Validating QBF Validity in HOL4. - Ramana Kumar; Tjark Weber (ITP, 2011)

Mathematizing C++ concurrency. - Mark Batty; Scott Owens; Susmit Sarkar; Peter Sewell; Tjark Weber (POPL, 2011)

Nitpicking C++ concurrency. - Jasmin Christian Blanchette; Tjark Weber; Mark Batty; Scott Owens; Susmit Sarkar (PPDP, 2011)

Designing Proof Formats: A User's Perspective. - Sascha Böhme; Tjark Weber (PxTP, 2011)

SMT solvers: new oracles for the HOL theorem prover. - Tjark Weber (Int. J. Softw. Tools Technol. Transf., 2011)

On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code - Hendrik Tews; Marcus Völp; Tjark Weber (SSV, 2012)

Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. - Alasdair Armstrong; Georg Struth; Tjark Weber (ITP, 2013)

Kleene Algebra. - Alasdair Armstrong; Georg Struth; Tjark Weber (Arch. Formal Proofs, 2013)

Relation Algebra. - Georg Struth; Tjark Weber (Arch. Formal Proofs, 2014)

Programming and automating mathematics in the Tarski-Kleene hierarchy. - Alasdair Armstrong; Georg Struth; Tjark Weber (J. Log. Algebraic Methods Program., 2014)

The 2014 SMT Competition. - David R. Cok; David Déharbe; Tjark Weber (J. Satisf. Boolean Model. Comput., 2014)

The 2013 Evaluation of SMT-COMP and SMT-LIB. - David R. Cok; Aaron Stump; Tjark Weber (J. Autom. Reason., 2015)

Scrambling and Descrambling SMT-LIB Benchmarks. - Tjark Weber (SMT@IJCAR, 2016)

Kleene Algebras with Domain. - Victor B. F. Gomes; Walter Guttmann; Peter Höfner; Georg Struth; Tjark Weber (Arch. Formal Proofs, 2016)

Modal Logics for Nominal Transition Systems. - Tjark Weber; Lars-Henrik Eriksson; Joachim Parrow; Johannes Borgström; Ramunas Gutkovas (Arch. Formal Proofs, 2016)

The Largest Respectful Function. - Joachim Parrow; Tjark Weber (Log. Methods Comput. Sci., 2016)

Psi-Calculi in Isabelle. - Jesper Bengtson; Joachim Parrow; Tjark Weber (J. Autom. Reason., 2016)

Weak Nominal Modal Logic. - Joachim Parrow; Tjark Weber; Johannes Borgström; Lars-Henrik Eriksson (FORTE, 2017)

Model-Theoretic Conservative Extension for Definitional Theories. - Arve Gengelbach; Tjark Weber (LSFA, 2017)

TOOLympics 2019: An Overview of Competitions in Formal Methods. - Ezio Bartocci; Dirk Beyer 001; Paul E. Black; Grigory Fedyukovich; Hubert Garavel; Arnd Hartmanns; Marieke Huisman; Fabrice Kordon; Julian Nagele; Mihaela Sighireanu; Bernhard Steffen; Martin Suda 001; et al. (TACAS (3), 2019)

The SMT Competition 2015-2018. - Tjark Weber; Sylvain Conchon; David Déharbe; Matthias Heizmann; Aina Niemetz; Giles Reger (J. Satisf. Boolean Model. Comput., 2019)

Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading. - Arve Gengelbach; Tjark Weber (ICTAC, 2020)

Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. - Arve Gengelbach; Johannes Åman Pohjola; Tjark Weber (LFMTP, 2020)

Hammering Floating-Point Arithmetic. - Olle Torstensson; Tjark Weber (FroCoS, 2023)

Verified QBF Solving. - Axel Bergström; Tjark Weber (Arch. Formal Proofs, 2024)

Broadcast Psi-calculi. - Palle Raabjerg; Johannes Åman Pohjola; Tjark Weber (Arch. Formal Proofs, 2024)

Finding Universally Quantified Heap Invariants by Horn Clause Transformations. - Zafer Esen; Philipp Rümmer; Tjark Weber (FSEN, 2025)

Sound and Complete Invariant-Based Heap Encodings (Technical Report). - Zafer Esen; Philipp Rümmer; Tjark Weber (CoRR, 2025)