Tjark Weber

Senior Lecturer/Associate Professor at Department of Information Technology; Division of Computing Science

Telephone:: +46 18 471 10 99
E-mail:: tjark.weber@it.uu.se
Visiting address:: Hus 10, Regementsvägen 10
Postal address:: Box 337
751 05 UPPSALA

Download contact information for Tjark Weber at Department of Information Technology; Division of Computing Science

Academic merits:: Docent

Short presentation

I am a member of the Concurrency research group at the Department of Information Technology, Uppsala University. My research interests include automated and interactive theorem proving, formal verification, programming languages, digital security and computational logic.

Please see http://user.it.uu.se/~tjawe125/ for further details.

Keywords

programming languages
theorem proving
formal verification
digital security
computational logic

Publications

Recent publications

Finding Universally Quantified Heap Invariants by Horn Clause Transformations

Esen, Zafer; Rümmer, Philipp; Weber, Tjark

Part of Fundamentals of Software Engineering - 11th IFIP WG 2.2 International Conference, FSEN 2025, Västerås, Sweden, April 7-8, 2025, Proceedings, p. 42-60, 2025
- DOI for Finding Universally Quantified Heap Invariants by Horn Clause Transformations
Hammering Floating-Point Arithmetic

Torstensson, Olle; Weber, Tjark

Part of FRONTIERS OF COMBINING SYSTEMS, FROCOS 2023, p. 217-235, 2023
- DOI for Hammering Floating-Point Arithmetic
- Download full text (pdf) of Hammering Floating-Point Arithmetic
Modal Logics for Nominal Transition Systems

Parrow, Joachim; Borgström, Johannes; Eriksson, Lars-Henrik; Forsberg Gutkovas, Ramunas et al.

Part of Logical Methods in Computer Science, 2021
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading

Gengelbach, Arve; Åman Pohjola, Johannes; Weber, Tjark

Part of Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages, p. 1-17, 2021
- DOI for Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
- Download full text (pdf) of Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Proof-theoretic Conservativity for HOL with Ad-hoc Overloading

Gengelbach, Arve; Weber, Tjark

Part of Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, p. 23-42, 2020
- DOI for Proof-theoretic Conservativity for HOL with Ad-hoc Overloading

All publications

Articles in journal

Modal Logics for Nominal Transition Systems

Parrow, Joachim; Borgström, Johannes; Eriksson, Lars-Henrik; Forsberg Gutkovas, Ramunas et al.

Part of Logical Methods in Computer Science, 2021
Model-theoretic Conservative Extension of Definitional Theories

Gengelbach, Arve; Weber, Tjark

Part of Electronic Notes in Theoretical Computer Science, p. 133-145, 2018
- DOI for Model-theoretic Conservative Extension of Definitional Theories
- Download full text (pdf) of Model-theoretic Conservative Extension of Definitional Theories
The largest respectful function

Parrow, Joachim; Weber, Tjark

Part of Logical Methods in Computer Science, 2016
- DOI for The largest respectful function
- Download full text (pdf) of The largest respectful function
Modal Logics for Nominal Transition Systems

Weber, Tjark; Eriksson, Lars-Henrik; Parrow, Joachim; Borgström, Johannes et al.

Part of Archive of Formal Proofs, 2016
Kleene Algebras with Domain

Gomes, Victor B. F.; Guttmann, Walter; Höfner, Peter; Struth, Georg et al.

Part of Archive of Formal Proofs, 2016
The 2014 SMT Competition

Weber, Tjark; Cok, David R.; Deharbe, David

Part of Journal on Satisfiability, Boolean Modeling and Computation, 2016
Psi-Calculi in Isabelle

Bengtson, Jesper; Parrow, Joachim; Weber, Tjark

Part of Journal of automated reasoning, p. 1-47, 2016
- DOI for Psi-Calculi in Isabelle
The 2013 Evaluation of SMT-COMP and SMT-LIB

Cok, David R.; Stump, Aaron; Weber, Tjark

Part of Journal of automated reasoning, p. 61-90, 2015
- DOI for The 2013 Evaluation of SMT-COMP and SMT-LIB
Programming and automating mathematics in the Tarski-Kleene hierarchy

Armstrong, Alasdair; Struth, Georg; Weber, Tjark

Part of Journal of Logical and Algebraic Methods in Programming, p. 87-102, 2014
- DOI for Programming and automating mathematics in the Tarski-Kleene hierarchy
Kleene Algebra

Armstrong, Alasdair; Struth, Georg; Weber, Tjark

Part of Archive of Formal Proofs, 2013

Conference papers

Conference proceedings (editor)

Proof Exchange for Theorem Proving: PxTP 2012

Pichardie, David; Weber, Tjark

2012

Manuscripts (preprints)

Sound and Complete Invariant-Based Heap Encodings

Esen, Zafer; Rümmer, Philipp; Weber, Tjark