Publications

In reverse chronological order, including workshop proceedings, technical reports and theses. See the DBLP Bibliography Server for a more concise (but somewhat incomplete) list.
  1. Broadcast Psi-calculi
    Palle Raabjerg, Johannes Åman Pohjola, and Tjark Weber. Archive of Formal Proofs, March 2024. Formal proof development.
  2. Verified QBF Solving
    Axel Bergström and Tjark Weber. Archive of Formal Proofs, March 2024. Formal proof development.
  3. Hammering Floating-Point Arithmetic
    Olle Torstensson and Tjark Weber. In Uli Sattler and Martin Suda, editors, Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings, volume 14279 of Lecture Notes in Computer Science, pages 217-235. Springer, 2023.
  4. Oracle Integration of Floating-Point Solvers with Isabelle
    Olle Torstensson and Tjark Weber. EasyChair Preprint no. 8640, 2022. Presented at the Isabelle Workshop 2022 (associated with ITP 2022/FLoC 2022).
  5. Modal Logics for Nominal Transition Systems
    Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Forsberg Gutkovas, and Tjark Weber. Log. Methods Comput. Sci., 17(1), 2021.
  6. Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Online (initially located in Paris, France), July 5-6, 2020
    François Bobot and Tjark Weber, editors. Volume 2854 of CEUR Workshop Proceedings. CEUR-WS.org, 2021.
  7. Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading
    Arve Gengelbach and Tjark Weber. In Violet Ka I Pun, Volker Stolz, and Adenilso Simão, editors, Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings, volume 12545 of Lecture Notes in Computer Science, pages 23-42. Springer, 2020.
  8. Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
    Arve Gengelbach, Johannes Åman Pohjola, and Tjark Weber. In Claudio Sacerdoti Coen and Alwen Tiu, editors, Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020, volume 332 of EPTCS, pages 1-17, 2020.
  9. The SMT Competition 2015-2018
    Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, and Giles Reger. J. Satisf. Boolean Model. Comput., 11(1):221-259, 2019.
  10. TOOLympics 2019: An Overview of Competitions in Formal Methods
    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, and Akihisa Yamada. In Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer Science, pages 3-24. Springer, 2019.
  11. Modal Logics for Nominal Transition Systems
    Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Forsberg Gutkovas, and Tjark Weber. CoRR, abs/1904.02564, 2019.
  12. Model-Theoretic Conservative Extension for Definitional Theories
    Arve Gengelbach and Tjark Weber. In Sandra Alves and Renata Wasserman, editors, 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017, volume 338 of Electronic Notes in Theoretical Computer Science, pages 133-145. Elsevier, 2017.
  13. Weak Nominal Modal Logic
    Joachim Parrow, Tjark Weber, Johannes Borgström, and Lars-Henrik Eriksson. In Ahmed Bouajjani and Alexandra Silva, editors, Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings, volume 10321 of Lecture Notes in Computer Science, pages 179-193. Springer, 2017.
  14. Modal Logics for Nominal Transition Systems
    Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström, and Ramūnas Gutkovas. Archive of Formal Proofs, October 2016. Formal proof development.
  15. Scrambling and Descrambling SMT-LIB Benchmarks
    Tjark Weber. In Tim King and Ruzica Piskac, editors, Proceedings of the 14th International Workshop on Satisfiability Modulo Theories, Coimbra, Portugal, July 1-2, 2016, volume 1617 of CEUR Workshop Proceedings, pages 31-40, July 2016.
  16. Kleene Algebras with Domain
    Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, and Tjark Weber. Archive of Formal Proofs, April 2016. Formal proof development.
  17. The Largest Respectful Function
    Joachim Parrow and Tjark Weber. Logical Methods in Computer Science, 12(2):1-8, 2016.
  18. Psi-Calculi in Isabelle
    Jesper Bengtson, Joachim Parrow, and Tjark Weber. Journal of Automated Reasoning, 56(1):1-47, 2016.
  19. The 2014 SMT Competition
    David R. Cok, David Déharbe, and Tjark Weber. Journal on Satisfiability, Boolean Modeling and Computation, 9(1):207-242, 2016.
  20. The 2013 Evaluation of SMT-COMP and SMT-LIB
    David R. Cok, Aaron Stump, and Tjark Weber. Journal of Automated Reasoning, 55(1):61-90, 2015.
  21. Resource Monitoring for Poly/ML Processes
    David Matthews, Magnus Stenqvist, and Tjark Weber. ACM SIGPLAN Workshop on ML, September 3, 2015, Vancouver, Canada, 2015.
  22. Modal Logics for Nominal Transition Systems
    Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, and Tjark Weber. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1-4, 2015, volume 42 of LIPIcs, pages 198-211. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2015.
  23. Modal Logics for Nominal Transition Systems
    Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, and Tjark Weber. Technical Report 2015-021, Department of Information Technology, Uppsala University, June 2015.
  24. Modal Logics for Nominal Transition Systems
    Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, and Tjark Weber. In Marino Miculan, editor, MeMo 2015 - 2nd International Workshop on Meta Models for Process Languages, Grenoble, June 5, 2015, Part of DisCoTec 2015, pages 44-61, 2015.
  25. The 2013 SMT Evaluation
    David R. Cok, Aaron Stump, and Tjark Weber. Technical Report 2014-017, Department of Information Technology, Uppsala University, July 2014.
  26. Programming and Automating Mathematics in the Tarski-Kleene Hierarchy
    Alasdair Armstrong, Georg Struth, and Tjark Weber. Journal of Logical and Algebraic Methods in Programming, 83(2):87-102, March 2014.
  27. Relation Algebra
    Alasdair Armstrong, Simon Foster, Georg Struth, and Tjark Weber. Archive of Formal Proofs, January 2014. Formal proof development.
  28. Program Analysis and Verification based on Kleene Algebra in Isabelle/HOL
    Alasdair Armstrong, Georg Struth, and Tjark Weber. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 197-212. Springer, 2013.
  29. Kleene Algebra
    Alasdair Armstrong, Georg Struth, and Tjark Weber. Archive of Formal Proofs, January 2013. Formal proof development.
  30. On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code
    Hendrik Tews, Marcus Völp, and Tjark Weber. In Franck Cassez, Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, Proceedings Seventh Conference on Systems Software Verification (SSV), volume 102 of EPTCS, pages 73-87, 2012.
  31. Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012), Manchester, UK, June 30, 2012
    David Pichardie and Tjark Weber, editors. Volume 878 of CEUR Workshop Proceedings, July 2012.
  32. Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
    Sascha Böhme, Anthony Fox, Thomas Sewell, and Tjark Weber. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 183-198. Springer, 2011.
  33. Automating Algebraic Methods in Isabelle
    Walter Guttmann, Georg Struth, and Tjark Weber. In Shengchao Qin and Zongyan Qiu, editors, Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings, volume 6991 of Lecture Notes in Computer Science, pages 617-632. Springer, 2011.
  34. SMT Solvers: New Oracles for the HOL Theorem Prover
    Tjark Weber. International Journal on Software Tools for Technology Transfer (STTT), 13(5):419-429, 2011.
  35. Validating QBF Validity in HOL4
    Ramana Kumar and Tjark Weber. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, volume 6898 of Lecture Notes in Computer Science, pages 168-183. Springer, 2011.
  36. Designing Proof Formats: A User's Perspective
    Sascha Böhme and Tjark Weber. In Pascal Fontaine and Aaron Stump, editors, PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, pages 27-32, August 2011.
  37. A Repository for Tarski-Kleene Algebras
    Walter Guttmann, Georg Struth, and Tjark Weber. In Peter Höfner, Annabelle McIver, and Georg Struth, editors, Proceedings of the First Workshop on Automated Theory Engineering, volume 760 of CEUR Workshop Proceedings, pages 30-39, July 2011.
  38. Nitpicking C++ Concurrency
    Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar. In Peter Schneider-Kamp and Michael Hanus, editors, Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark, pages 113-124. ACM, 2011.
  39. Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL - (Invited Tutorial)
    Simon Foster, Georg Struth, and Tjark Weber. In Harrie C. M. de Swart, editor, Relational and Algebraic Methods in Computer Science - 12th International Conference, RAMICS 2011, Rotterdam, The Netherlands, May 30 - June 3, 2011. Proceedings, volume 6663 of Lecture Notes in Computer Science, pages 52-67. Springer, 2011.
  40. Mathematizing C++ Concurrency
    Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 55-66. ACM, 2011.
  41. Mathematizing C++ Concurrency: The Post-Rapperswil Model
    Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Technical Report N3132, ISO IEC JTC1/SC22/WG21, August 2010. http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3132.pdf.
  42. Validating QBF Invalidity in HOL4
    Tjark Weber. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 466-480. Springer, 2010.
  43. Fast LCF-Style Proof Reconstruction for Z3
    Sascha Böhme and Tjark Weber. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 179-194. Springer, 2010.
  44. SMT Solvers: New Oracles for the HOL Theorem Prover
    Tjark Weber. Published at the Workshop on Verified Software: Theory, Tools, and Experiments (VSTTE 2009), November 2, 2009, Eindhoven, Netherlands.
  45. Alternatives vs. Outcomes: A Note on the Gibbard-Satterthwaite Theorem
    Tjark Weber. Published online at the Munich Personal RePEc Archive. MPRA Paper No. 17836, available at http://mpra.ub.uni-muenchen.de/17836/, October 2009.
  46. Finite Models in FOL-Based Crypto-Protocol Verification
    Jan Jürjens and Tjark Weber. In Pierpaolo Degano and Luca Viganò, editors, Foundations and Applications of Security Analysis, Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March 28-29, 2009, Revised Selected Papers, volume 5511 of Lecture Notes in Computer Science, pages 155-172. Springer, 2009.
  47. Finite Models in FOL-based Crypto-Protocol Verification
    Jan Jürjens and Tjark Weber. In Pierpaolo Degano and Luca Viganò, editors, ARSPA-WITS'09 - Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, Informal Proceedings, pages 211-227, York, UK, March 2009.
  48. Formal Memory Models for the Verification of Low-Level Operating-System Code
    Hendrik Tews, Marcus Völp, and Tjark Weber. Journal of Automated Reasoning: Special Issue on Operating Systems Verification, 42(2-4):189-227, April 2009.
  49. On Commutativity and Groupoid Identities between Products with 3 Factors
    Tjark Weber. International Journal of Algebra, 3(5):199-210, 2009.
  50. Nova Micro-Hypervisor Verification
    Hendrik Tews, Tjark Weber, Marcus Völp, Erik Poll, Marko van Eekelen, and Peter van Rossum. Technical Report ICIS-R08012, Radboud University Nijmegen, May 2008.
  51. Formal Nova Interface Specification
    Hendrik Tews, Tjark Weber, Erik Poll, Marko van Eekelen, and Peter van Rossum. Technical Report ICIS-R08011, Radboud University Nijmegen, May 2008.
  52. SAT-based Finite Model Generation for Higher-Order Logic
    Tjark Weber. PhD thesis, Institut für Informatik, Technische Universität München, Germany, April 2008.
  53. A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code
    Hendrik Tews, Tjark Weber, and Marcus Völp. In Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, Proceedings of the 3rd International Workshop on Systems Software Verification (SSV 08), Sydney, Australia, February 25-27, 2008, volume 217 of Electronic Notes in Theoretical Computer Science, pages 79-96. Elsevier, July 2008.
  54. Practical Proof Reconstruction for First-Order Logic and Set-Theoretical Constructions
    Clément Hurlin, Amine Chaieb, Pascal Fontaine, Stephan Merz, and Tjark Weber. In Lucas Dixon and Moa Johansson, editors, Proceedings of the Isabelle Workshop 2007, pages 2-13, Bremen, Germany, July 2007.
  55. Efficiently Checking Propositional Refutations in HOL Theorem Provers
    Tjark Weber and Hasan Amjad. Journal of Applied Logic, 7(1):26-40, March 2009.
  56. Efficiently Checking Propositional Resolution Proofs in Isabelle/HOL
    Tjark Weber. In Chris Benzmüller, Bernd Fischer, and Geoff Sutcliffe, editors, Proceedings of the 6th International Workshop on the Implementation of Logics, volume 212 of CEUR Workshop Proceedings, pages 44-62, November 2006.
  57. Logical Aspects of Secure Computer Systems: Proceedings of the NATO Advanced Study Institute on Logical Aspects of Secure Computer Systems, Held in Marktoberdorf, Germany, August 2-14, 2005.
    Katharina Spies and Tjark Weber, editors. IOS Press, 2005. To appear.
  58. A SAT-based Sudoku Solver
    Tjark Weber. In Geoff Sutcliffe and Andrei Voronkov, editors, LPAR-12, The 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Short Paper Proceedings, pages 11-15, December 2005.
  59. Towards Automated Proof Support for Probabilistic Distributed Systems
    Annabelle McIver and Tjark Weber. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, volume 3835 of Lecture Notes in Computer Science, pages 534-548. Springer, December 2005.
  60. Using a SAT Solver as a Fast Decision Procedure for Propositional Logic in an LCF-style Theorem Prover
    Tjark Weber. In Joe Hurd, Edward Smith, and Ashish Darbari, editors, Theorem Proving in Higher Order Logics - 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005, Emerging Trends Proceedings, pages 180-189, Oxford, UK, August 2005. Oxford University Computing Laboratory, Programming Research Group. Research Report PRG-RR-05-02.
  61. Integrating a SAT Solver with an LCF-style Theorem Prover
    Tjark Weber. In Alessandro Armando and Alessandro Cimatti, editors, Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005), volume 144(2) of Electronic Notes in Theoretical Computer Science, pages 67-78. Elsevier, January 2006.
  62. Bounded Model Generation for Isabelle/HOL
    Tjark Weber. In Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, and Cesare Tinelli, editors, Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 2004), volume 125(3) of Electronic Notes in Theoretical Computer Science, pages 103-116. Elsevier, July 2005.
  63. Towards Mechanized Program Verification with Separation Logic
    Tjark Weber. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic - 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 250-264. Springer, September 2004.
  64. Bounded Model Generation for Isabelle/HOL
    Tjark Weber. In 2nd International Joint Conference on Automated Reasoning (IJCAR 2004) Workshop W1: Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability, Cork, Ireland, July 2004.
  65. Constructively Characterizing Fold and Unfold
    Tjark Weber and James Caldwell. In Maurice Bruynooghe, editor, Logic Based Program Synthesis and Transformation - 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, Revised Selected Papers, volume 3018 of Lecture Notes in Computer Science, pages 110-127. Springer, June 2004.
  66. Constructively Characterizing Fold and Unfold
    Tjark Weber and James Caldwell. In Maurice Bruynooghe, editor, LOPSTR 2003 Preproceedings of the International Symposium on Logic Based Program Synthesis and Transformation, pages 149-164, Leuven, Belgium, August 2003. Department of Computer Science, K.U. Leuven. Report CW 365.
  67. Quicksort via Bird's Tree Fusion Transformation
    Tjark Weber and James Caldwell. Published online at the Formal Digital Libraries Project, May 2003.
  68. Program Transformations in Nuprl
    Tjark Weber. Master's thesis, University of Wyoming, Laramie, WY, August 2002.
Last modified: 2024-04-10 Home Valid HTML 4.01 Transitional Valid CSS