Tjark Weber

ORCID

Publication Activity (10 Years)

Years Active: 2003-2024
Publications (10 Years): 16

Top Venues

Arch. Formal Proofs

J. Autom. Reason.

J. Satisf. Boolean Model. Comput.

Log. Methods Comput. Sci.

Technical University Munich, Germany (PHD)

Education History

Technical University Munich, Germany

PHD

Publications

Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber
Broadcast Psi-calculi. Arch. Formal Proofs 2024 (2024)
Axel Bergström, Tjark Weber
Verified QBF Solving. Arch. Formal Proofs 2024 (2024)
Olle Torstensson, Tjark Weber
Hammering Floating-Point Arithmetic. FroCoS (2023)
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber
Modal Logics for Nominal Transition Systems. Log. Methods Comput. Sci. 17 (1) (2021)
Arve Gengelbach, Tjark Weber
Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading. ICTAC (2020)
Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. LFMTP (2020)
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber
Modal Logics for Nominal Transition Systems. CoRR (2019)
Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger
The SMT Competition 2015-2018. J. Satisf. Boolean Model. Comput. 11 (1) (2019)
Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, Akihisa Yamada
TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) (2019)
Joachim Parrow, Tjark Weber, Johannes Borgström, Lars-Henrik Eriksson
Weak Nominal Modal Logic. FORTE (2017)
Arve Gengelbach, Tjark Weber
Model-Theoretic Conservative Extension for Definitional Theories. LSFA (2017)
Tjark Weber
Scrambling and Descrambling SMT-LIB Benchmarks. SMT@IJCAR (2016)
Jesper Bengtson, Joachim Parrow, Tjark Weber
Psi-Calculi in Isabelle. J. Autom. Reason. 56 (1) (2016)
Joachim Parrow, Tjark Weber
The Largest Respectful Function. Log. Methods Comput. Sci. 12 (2) (2016)
Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
Kleene Algebras with Domain. Arch. Formal Proofs 2016 (2016)
Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström, Ramunas Gutkovas
Modal Logics for Nominal Transition Systems. Arch. Formal Proofs 2016 (2016)
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber
Modal Logics for Nominal Transition Systems. CONCUR (2015)
David R. Cok, Aaron Stump, Tjark Weber
The 2013 Evaluation of SMT-COMP and SMT-LIB. J. Autom. Reason. 55 (1) (2015)
David R. Cok, David Déharbe, Tjark Weber
The 2014 SMT Competition. J. Satisf. Boolean Model. Comput. 9 (1) (2014)
Alasdair Armstrong, Georg Struth, Tjark Weber
Programming and automating mathematics in the Tarski-Kleene hierarchy. J. Log. Algebraic Methods Program. 83 (2) (2014)
Georg Struth, Tjark Weber
Relation Algebra. Arch. Formal Proofs 2014 (2014)
Alasdair Armstrong, Georg Struth, Tjark Weber
Kleene Algebra. Arch. Formal Proofs 2013 (2013)
Alasdair Armstrong, Georg Struth, Tjark Weber
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. ITP (2013)
Hendrik Tews, Marcus Völp, Tjark Weber
On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code SSV (2012)
Ramana Kumar, Tjark Weber
Validating QBF Validity in HOL4. ITP (2011)
Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. CPP (2011)
Walter Guttmann, Georg Struth, Tjark Weber
A Repository for Tarski-Kleene Algebras. ATE (2011)
Simon Foster, Georg Struth, Tjark Weber
Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL - (Invited Tutorial). RAMiCS (2011)
Tjark Weber
SMT solvers: new oracles for the HOL theorem prover. Int. J. Softw. Tools Technol. Transf. 13 (5) (2011)
Walter Guttmann, Georg Struth, Tjark Weber
Automating Algebraic Methods in Isabelle. ICFEM (2011)
Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar
Nitpicking C++ concurrency. PPDP (2011)
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
Mathematizing C++ concurrency. POPL (2011)
Sascha Böhme, Tjark Weber
Designing Proof Formats: A User's Perspective. PxTP (2011)
Sascha Böhme, Tjark Weber
Fast LCF-Style Proof Reconstruction for Z3. ITP (2010)
Tjark Weber
Validating QBF Invalidity in HOL4. ITP (2010)
Hendrik Tews, Marcus Völp, Tjark Weber
Formal Memory Models for the Verification of Low-Level Operating-System Code. J. Autom. Reason. 42 (2-4) (2009)
Tjark Weber, Hasan Amjad
Efficiently checking propositional refutations in HOL theorem provers. J. Appl. Log. 7 (1) (2009)
Jan Jürjens, Tjark Weber
Finite Models in FOL-Based Crypto-Protocol Verification. ARSPA-WITS (2009)
Hendrik Tews, Tjark Weber, Marcus Völp
A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code. Electron. Notes Theor. Comput. Sci. 217 (2008)
Tjark Weber
Integrating a SAT Solver with an LCF-style Theorem Prover. Electron. Notes Theor. Comput. Sci. 144 (2) (2006)
Tjark Weber
Bounded Model Generation for Isabelle/HOL. Electron. Notes Theor. Comput. Sci. 125 (3) (2005)
Annabelle McIver, Tjark Weber
Towards Automated Proof Support for Probabilistic Distributed Systems. LPAR (2005)
Tjark Weber
Towards Mechanized Program Verification with Separation Logic. CSL (2004)
Tjark Weber, James L. Caldwell
Constructively Characterizing Fold and Unfold. LOPSTR (2003)

Tjark Weber.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Tjark Weber