Tjark Weber
Universitetslektor vid Institutionen för informationsteknologi; Datalogi
- Telefon:
- 018-471 10 99
- E-post:
- tjark.weber@it.uu.se
- Besöksadress:
- Hus 10, Regementsvägen 10
- Postadress:
- Box 337
751 05 UPPSALA
Ladda ned kontaktuppgifter för Tjark Weber vid Institutionen för informationsteknologi; Datalogi
- Akademiska meriter:
- Docent
Kort 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.
Nyckelord
- programming languages
- theorem proving
- formal verification
- digital security
- computational logic
Publikationer
Senaste publikationer
-
Sound and Complete Invariant-Based Heap Encodings
Ingår i Proceedings of the ACM on Programming Languages, s. 794-822, 2026
- DOI för Sound and Complete Invariant-Based Heap Encodings
- Ladda ner fulltext (pdf) av Sound and Complete Invariant-Based Heap Encodings
-
Finding Universally Quantified Heap Invariants by Horn Clause Transformations
Ingår i Fundamentals of Software Engineering - 11th IFIP WG 2.2 International Conference, FSEN 2025, Västerås, Sweden, April 7-8, 2025, Proceedings, s. 42-60, 2025
-
Hammering Floating-Point Arithmetic
Ingår i FRONTIERS OF COMBINING SYSTEMS, FROCOS 2023, s. 217-235, 2023
- DOI för Hammering Floating-Point Arithmetic
- Ladda ner fulltext (pdf) av Hammering Floating-Point Arithmetic
-
Modal Logics for Nominal Transition Systems
Ingår i Logical Methods in Computer Science, 2021
- DOI för Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 1 (pdf) av Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 2 (pdf) av Modal Logics for Nominal Transition Systems
-
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Ingår i Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages, s. 1-17, 2021
- DOI för Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
- Ladda ner fulltext (pdf) av Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Alla publikationer
Artiklar i tidskrift
-
Sound and Complete Invariant-Based Heap Encodings
Ingår i Proceedings of the ACM on Programming Languages, s. 794-822, 2026
- DOI för Sound and Complete Invariant-Based Heap Encodings
- Ladda ner fulltext (pdf) av Sound and Complete Invariant-Based Heap Encodings
-
Modal Logics for Nominal Transition Systems
Ingår i Logical Methods in Computer Science, 2021
- DOI för Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 1 (pdf) av Modal Logics for Nominal Transition Systems
- Ladda ner fulltext 2 (pdf) av Modal Logics for Nominal Transition Systems
-
Model-theoretic Conservative Extension of Definitional Theories
Ingår i Electronic Notes in Theoretical Computer Science, s. 133-145, 2018
- DOI för Model-theoretic Conservative Extension of Definitional Theories
- Ladda ner fulltext (pdf) av Model-theoretic Conservative Extension of Definitional Theories
-
The largest respectful function
Ingår i Logical Methods in Computer Science, 2016
-
Modal Logics for Nominal Transition Systems
Ingår i Archive of Formal Proofs, 2016
-
Ingår i Archive of Formal Proofs, 2016
-
Ingår i Journal on Satisfiability, Boolean Modeling and Computation, 2016
-
Ingår i Journal of automated reasoning, s. 1-47, 2016
-
The 2013 Evaluation of SMT-COMP and SMT-LIB
Ingår i Journal of automated reasoning, s. 61-90, 2015
-
Programming and automating mathematics in the Tarski-Kleene hierarchy
Ingår i Journal of Logical and Algebraic Methods in Programming, s. 87-102, 2014
-
Ingår i Archive of Formal Proofs, 2013
Konferensbidrag
-
Finding Universally Quantified Heap Invariants by Horn Clause Transformations
Ingår i Fundamentals of Software Engineering - 11th IFIP WG 2.2 International Conference, FSEN 2025, Västerås, Sweden, April 7-8, 2025, Proceedings, s. 42-60, 2025
-
Hammering Floating-Point Arithmetic
Ingår i FRONTIERS OF COMBINING SYSTEMS, FROCOS 2023, s. 217-235, 2023
- DOI för Hammering Floating-Point Arithmetic
- Ladda ner fulltext (pdf) av Hammering Floating-Point Arithmetic
-
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Ingår i Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages, s. 1-17, 2021
- DOI för Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
- Ladda ner fulltext (pdf) av Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
-
Proof-theoretic Conservativity for HOL with Ad-hoc Overloading
Ingår i Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, s. 23-42, 2020
-
TOOLympics 2019: An overview of competitions in formal methods
Ingår i Tools and Algorithms for the Construction and Analysis of Systems, s. 3-24, 2019
- DOI för TOOLympics 2019: An overview of competitions in formal methods
- Ladda ner fulltext (pdf) av TOOLympics 2019: An overview of competitions in formal methods
-
Ingår i Formal Techniques for Distributed Objects, Components, and Systems, s. 179-193, 2017
-
Scrambling and descrambling SMT-LIB benchmarks
Ingår i Satisfiability Modulo Theories, s. 31-40, 2016
-
Modal Logics for Nominal Transition Systems
Ingår i 26th International Conference on Concurrency Theory, s. 198-211, 2015
-
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
Ingår i Interactive Theorem Proving, s. 197-212, 2013
- DOI för Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
- Ladda ner fulltext (pdf) av Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
-
On the use of underspecified data-type semantics for type safety in low-level code
Ingår i Proc. 7th Conference on Systems Software Verification, s. 73-87, 2012