Tjark Weber

According to our database, Tjark Weber authored at least 41 papers between 2003 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Verified QBF Solving.

Axel Bergström, Tjark Weber

Arch. Formal Proofs, 2024

2023

Hammering Floating-Point Arithmetic.

Olle Torstensson, Tjark Weber

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

2021

Modal Logics for Nominal Transition Systems.

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber

Log. Methods Comput. Sci., 2021

2020

Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading.

Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber

Proceedings of the Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2020

Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading.

Arve Gengelbach, Tjark Weber

Proceedings of the Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30, 2020

2019

The SMT Competition 2015-2018.

Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger

J. Satisf. Boolean Model. Comput., 2019

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, Akihisa Yamada

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

2017

Model-Theoretic Conservative Extension for Definitional Theories.

Arve Gengelbach, Tjark Weber

Proceedings of the 12th Workshop on Logical and Semantic Frameworks, with Applications, 2017

Weak Nominal Modal Logic.

Joachim Parrow, Tjark Weber, Johannes Borgström, Lars-Henrik Eriksson

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

2016

Psi-Calculi in Isabelle.

Jesper Bengtson, Joachim Parrow, Tjark Weber

J. Autom. Reason., 2016

The Largest Respectful Function.

Joachim Parrow, Tjark Weber

Log. Methods Comput. Sci., 2016

Kleene Algebras with Domain.

Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber

Arch. Formal Proofs, 2016

Scrambling and Descrambling SMT-LIB Benchmarks.

Tjark Weber

Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, 2016

2015

The 2013 Evaluation of SMT-COMP and SMT-LIB.

David R. Cok, Aaron Stump, Tjark Weber

J. Autom. Reason., 2015

2014

The 2014 SMT Competition.

David R. Cok, David Déharbe, Tjark Weber

J. Satisf. Boolean Model. Comput., 2014

Programming and automating mathematics in the Tarski-Kleene hierarchy.

Alasdair Armstrong, Georg Struth, Tjark Weber

J. Log. Algebraic Methods Program., 2014

Relation Algebra.

Georg Struth, Tjark Weber

Arch. Formal Proofs, 2014

2013

Kleene Algebra.

Alasdair Armstrong, Georg Struth, Tjark Weber

Arch. Formal Proofs, 2013

Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL.

Alasdair Armstrong, Georg Struth, Tjark Weber

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code

Hendrik Tews, Marcus Völp, Tjark Weber

Proceedings of the Proceedings Seventh Conference on Systems Software Verification, 2012

2011

SMT solvers: new oracles for the HOL theorem prover.

Tjark Weber

Int. J. Softw. Tools Technol. Transf., 2011

Designing Proof Formats: A User's Perspective.

Sascha Böhme, Tjark Weber

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

Nitpicking C++ concurrency.

Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar

Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Mathematizing C++ concurrency.

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Validating QBF Validity in HOL4.

Ramana Kumar, Tjark Weber

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Automating Algebraic Methods in Isabelle.

Walter Guttmann, Georg Struth, Tjark Weber

Proceedings of the Formal Methods and Software Engineering, 2011

Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.

Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

A Repository for Tarski-Kleene Algebras.

Walter Guttmann, Georg Struth, Tjark Weber

Proceedings of the First Workshop on Automated Theory Engineering, 2011

Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL - (Invited Tutorial).

Simon Foster, Georg Struth, Tjark Weber

Proceedings of the Relational and Algebraic Methods in Computer Science, 2011

2010

Validating QBF Invalidity in HOL4.

Tjark Weber

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Fast LCF-Style Proof Reconstruction for Z3.

Sascha Böhme, Tjark Weber

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Formal Memory Models for the Verification of Low-Level Operating-System Code.

Hendrik Tews, Marcus Völp, Tjark Weber

J. Autom. Reason., 2009

Efficiently checking propositional refutations in HOL theorem provers.

Tjark Weber, Hasan Amjad

J. Appl. Log., 2009

Finite Models in FOL-Based Crypto-Protocol Verification.

Jan Jürjens, Tjark Weber

Proceedings of the Foundations and Applications of Security Analysis, 2009

2008

SAT-based finite model generation for higher-order logic.

Tjark Weber

PhD thesis, 2008

A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code.

Hendrik Tews, Tjark Weber, Marcus Völp

Proceedings of the 3rd International Workshop on Systems Software Verification, 2008

2005

Integrating a SAT Solver with an LCF-style Theorem Prover.

Tjark Weber

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Towards Automated Proof Support for Probabilistic Distributed Systems.

Annabelle McIver, Tjark Weber

Proceedings of the Logic for Programming, 2005

2004

Bounded Model Generation for Isabelle/HOL.

Tjark Weber

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Towards Mechanized Program Verification with Separation Logic.

Tjark Weber

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

Constructively Characterizing Fold and Unfold.

Tjark Weber, James L. Caldwell

Proceedings of the Logic Based Program Synthesis and Transformation, 2003