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
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
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
Alla publikationer
Artiklar i tidskrift
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