Tjark Weber

49 papers A* 1B 8C 6Journal 18Unranked 13
YearRankTypeTitle / Venue / Authors
2025 — conf
Finding Universally Quantified Heap Invariants by Horn Clause Transformations.
FSEN
Zafer Esen, Philipp Rümmer, Tjark Weber
2025 J jnl
Sound and Complete Invariant-Based Heap Encodings (Technical Report).
CoRR
Zafer Esen, Philipp Rümmer, Tjark Weber
2024 J jnl
Broadcast Psi-calculi.
Arch. Formal Proofs
Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber
2024 J jnl
Verified QBF Solving.
Arch. Formal Proofs
Axel Bergström, Tjark Weber
2023 — conf
Hammering Floating-Point Arithmetic.
FroCoS
Olle Torstensson, Tjark Weber
2021 J jnl
Modal Logics for Nominal Transition Systems.
Log. Methods Comput. Sci.
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber
2021 — ed.
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.
SMT
François Bobot, Tjark Weber
2020 — conf
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading.
LFMTP
Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber
2020 C conf
Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading.
ICTAC
Arve Gengelbach, Tjark Weber
2019 J jnl
Modal Logics for Nominal Transition Systems.
CoRR
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber
2019 — conf
TOOLympics 2019: An Overview of Competitions in Formal Methods.
TACAS (3)
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
2019 J jnl
The SMT Competition 2015-2018.
J. Satisf. Boolean Model. Comput.
Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger
2017 — conf
Model-Theoretic Conservative Extension for Definitional Theories.
LSFA
Arve Gengelbach, Tjark Weber
2017 C conf
Weak Nominal Modal Logic.
FORTE
Joachim Parrow, Tjark Weber, Johannes Borgström, Lars-Henrik Eriksson
2016 J jnl
Kleene Algebras with Domain.
Arch. Formal Proofs
Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
2016 J jnl
Modal Logics for Nominal Transition Systems.
Arch. Formal Proofs
Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström, Ramunas Gutkovas
2016 J jnl
Psi-Calculi in Isabelle.
J. Autom. Reason.
Jesper Bengtson, Joachim Parrow, Tjark Weber
2016 — conf
Scrambling and Descrambling SMT-LIB Benchmarks.
SMT@IJCAR
Tjark Weber
2016 J jnl
The Largest Respectful Function.
Log. Methods Comput. Sci.
Joachim Parrow, Tjark Weber
2015 B conf
Modal Logics for Nominal Transition Systems.
CONCUR
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber
2015 J jnl
The 2013 Evaluation of SMT-COMP and SMT-LIB.
J. Autom. Reason.
David R. Cok, Aaron Stump, Tjark Weber
2014 J jnl
Programming and automating mathematics in the Tarski-Kleene hierarchy.
J. Log. Algebraic Methods Program.
Alasdair Armstrong, Georg Struth, Tjark Weber
2014 J jnl
Relation Algebra.
Arch. Formal Proofs
Georg Struth, Tjark Weber
2014 J jnl
The 2014 SMT Competition.
J. Satisf. Boolean Model. Comput.
David R. Cok, David Déharbe, Tjark Weber
2013 J jnl
Kleene Algebra.
Arch. Formal Proofs
Alasdair Armstrong, Georg Struth, Tjark Weber
2013 B conf
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL.
ITP
Alasdair Armstrong, Georg Struth, Tjark Weber
2012 — conf
On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code
SSV
Hendrik Tews, Marcus Völp, Tjark Weber
2012 — ed.
Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012
PxTP
David Pichardie, Tjark Weber
2011 — conf
A Repository for Tarski-Kleene Algebras.
ATE
Walter Guttmann, Georg Struth, Tjark Weber
2011 C conf
Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL - (Invited Tutorial).
RAMiCS
Simon Foster, Georg Struth, Tjark Weber
2011 C conf
Automating Algebraic Methods in Isabelle.
ICFEM
Walter Guttmann, Georg Struth, Tjark Weber
2011 — conf
Designing Proof Formats: A User's Perspective.
PxTP
Sascha Böhme, Tjark Weber
2011 A* conf
Mathematizing C++ concurrency.
POPL
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
2011 C conf
Nitpicking C++ concurrency.
PPDP
Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar
2011 B conf
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.
CPP
Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber
2011 J jnl
SMT solvers: new oracles for the HOL theorem prover.
Int. J. Softw. Tools Technol. Transf.
Tjark Weber
2011 B conf
Validating QBF Validity in HOL4.
ITP
Ramana Kumar, Tjark Weber
2010 B conf
Fast LCF-Style Proof Reconstruction for Z3.
ITP
Sascha Böhme, Tjark Weber
2010 B conf
Validating QBF Invalidity in HOL4.
ITP
Tjark Weber
2009 J jnl
Efficiently checking propositional refutations in HOL theorem provers.
J. Appl. Log.
Tjark Weber, Hasan Amjad
2009 — conf
Finite Models in FOL-Based Crypto-Protocol Verification.
ARSPA-WITS
Jan Jürjens, Tjark Weber
2009 J jnl
Formal Memory Models for the Verification of Low-Level Operating-System Code.
J. Autom. Reason.
Hendrik Tews, Marcus Völp, Tjark Weber
2008 — conf
A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code.
SSV
Hendrik Tews, Tjark Weber, Marcus Völp
2008 — —
SAT-based finite model generation for higher-order logic.
Tjark Weber
2005 — conf
Integrating a SAT Solver with an LCF-style Theorem Prover.
PDPAR@CAV
Tjark Weber
2005 B conf
Towards Automated Proof Support for Probabilistic Distributed Systems.
LPAR
Annabelle McIver, Tjark Weber
2004 — conf
Bounded Model Generation for Isabelle/HOL.
D/PDPAR@IJCAR
Tjark Weber
2004 B conf
Towards Mechanized Program Verification with Separation Logic.
CSL
Tjark Weber
2003 C conf
Constructively Characterizing Fold and Unfold.
LOPSTR
Tjark Weber, James L. Caldwell