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, Lägerhyddsvägen 1
- Postal address:
- Box 337
751 05 UPPSALA
- Academic merits:
- Docent
More information is available to staff who log in.
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
- computational logic
- digital security
- formal verification
- programming languages
- theorem proving
Publications
Recent publications
- Hammering Floating-Point Arithmetic (2023)
- Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading (2021)
- Modal Logics for Nominal Transition Systems (2021)
- Proof-theoretic Conservativity for HOL with Ad-hoc Overloading (2020)
- TOOLympics 2019 (2019)
All publications
Articles
- Modal Logics for Nominal Transition Systems (2021)
- Model-theoretic Conservative Extension of Definitional Theories (2018)
- Psi-Calculi in Isabelle (2016)
- Kleene Algebras with Domain (2016)
- The largest respectful function (2016)
- The 2014 SMT Competition (2016)
- Modal Logics for Nominal Transition Systems (2016)
- The 2013 Evaluation of SMT-COMP and SMT-LIB (2015)
- Programming and automating mathematics in the Tarski-Kleene hierarchy (2014)
- Kleene Algebra (2013)
Books
Conferences
- Hammering Floating-Point Arithmetic (2023)
- Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading (2021)
- Proof-theoretic Conservativity for HOL with Ad-hoc Overloading (2020)
- TOOLympics 2019 (2019)
- Weak Nominal Modal Logic (2017)
- Scrambling and descrambling SMT-LIB benchmarks (2016)
- Modal Logics for Nominal Transition Systems (2015)
- Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL (2013)
- On the use of underspecified data-type semantics for type safety in low-level code (2012)
