default search action
Tjark Weber
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j16]Axel Bergström, Tjark Weber:
Verified QBF Solving. Arch. Formal Proofs 2024 (2024) - [j15]Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber:
Broadcast Psi-calculi. Arch. Formal Proofs 2024 (2024) - 2023
- [c27]Olle Torstensson
, Tjark Weber
Hammering Floating-Point Arithmetic. FroCoS 2023: 217-235 - 2021
- [j14]Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber:
Modal Logics for Nominal Transition Systems. Log. Methods Comput. Sci. 17(1) (2021) - [e2]François Bobot, Tjark Weber:
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. CEUR Workshop Proceedings 2854, CEUR-WS.org 2021 [contents] - 2020
- [c26]Arve Gengelbach
Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading. ICTAC 2020: 23-42 - [c25]Arve Gengelbach, Johannes Åman Pohjola
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. LFMTP 2020: 1-17
2010 – 2019
- 2019
- [j13]Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger:
The SMT Competition 2015-2018. J. Satisf. Boolean Model. Comput. 11(1): 221-259 (2019) - [c24]Ezio Bartocci
TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) 2019: 3-24 - [i1]Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber:
Modal Logics for Nominal Transition Systems. CoRR abs/1904.02564 (2019) - 2017
- [c23]Joachim Parrow, Tjark Weber, Johannes Borgström, Lars-Henrik Eriksson:
Weak Nominal Modal Logic. FORTE 2017: 179-193 - [c22]Arve Gengelbach, Tjark Weber:
Model-Theoretic Conservative Extension for Definitional Theories. LSFA 2017: 133-145 - 2016
- [j12]Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber:
Kleene Algebras with Domain. Arch. Formal Proofs 2016 (2016) - [j11]Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström, Ramunas Gutkovas:
Modal Logics for Nominal Transition Systems. Arch. Formal Proofs 2016 (2016) - [j10]Joachim Parrow, Tjark Weber:
The Largest Respectful Function. Log. Methods Comput. Sci. 12(2) (2016) - [j9]Jesper Bengtson, Joachim Parrow, Tjark Weber:
Psi-Calculi in Isabelle. J. Autom. Reason. 56(1): 1-47 (2016) - [c21]Tjark Weber:
Scrambling and Descrambling SMT-LIB Benchmarks. SMT@IJCAR 2016: 31-40 - 2015
- [j8]David R. Cok, Aaron Stump, Tjark Weber:
The 2013 Evaluation of SMT-COMP and SMT-LIB. J. Autom. Reason. 55(1): 61-90 (2015) - [c20]Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber:
Modal Logics for Nominal Transition Systems. CONCUR 2015: 198-211 - 2014
- [j7]Georg Struth, Tjark Weber:
Relation Algebra. Arch. Formal Proofs 2014 (2014) - [j6]Alasdair Armstrong, Georg Struth, Tjark Weber:
Programming and automating mathematics in the Tarski-Kleene hierarchy. J. Log. Algebraic Methods Program. 83(2): 87-102 (2014) - [j5]David R. Cok, David Déharbe, Tjark Weber:
The 2014 SMT Competition. J. Satisf. Boolean Model. Comput. 9(1): 207-242 (2014) - 2013
- [j4]Alasdair Armstrong, Georg Struth, Tjark Weber:
Kleene Algebra. Arch. Formal Proofs 2013 (2013) - [c19]Alasdair Armstrong, Georg Struth, Tjark Weber:
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. ITP 2013: 197-212 - 2012
- [c18]Hendrik Tews, Marcus Völp
On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code. SSV 2012: 73-87 - [e1]David Pichardie, Tjark Weber:
Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012. CEUR Workshop Proceedings 878, CEUR-WS.org 2012 [contents] - 2011
- [j3]Tjark Weber:
SMT solvers: new oracles for the HOL theorem prover. Int. J. Softw. Tools Technol. Transf. 13(5): 419-429 (2011) - [c17]Simon Foster
Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL - (Invited Tutorial). RAMiCS 2011: 52-67 - [c16]Walter Guttmann, Georg Struth, Tjark Weber:
A Repository for Tarski-Kleene Algebras. ATE 2011: 30-39 - [c15]Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber:
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. CPP 2011: 183-198 - [c14]Walter Guttmann
Automating Algebraic Methods in Isabelle. ICFEM 2011: 617-632 - [c13]Ramana Kumar, Tjark Weber:
Validating QBF Validity in HOL4. ITP 2011: 168-183 - [c12]Mark Batty, Scott Owens
Mathematizing C++ concurrency. POPL 2011: 55-66 - [c11]Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens
Nitpicking C++ concurrency. PPDP 2011: 113-124 - [c10]Sascha Böhme, Tjark Weber:
Designing Proof Formats: A User's Perspective. PxTP 2011: 27-32 - 2010
- [c9]Sascha Böhme, Tjark Weber:
Fast LCF-Style Proof Reconstruction for Z3. ITP 2010: 179-194 - [c8]Tjark Weber:
Validating QBF Invalidity in HOL4. ITP 2010: 466-480
2000 – 2009
- 2009
- [j2]Tjark Weber, Hasan Amjad:
Efficiently checking propositional refutations in HOL theorem provers. J. Appl. Log. 7(1): 26-40 (2009) - [j1]Hendrik Tews, Marcus Völp
Formal Memory Models for the Verification of Low-Level Operating-System Code. J. Autom. Reason. 42(2-4): 189-227 (2009) - [c7]Jan Jürjens, Tjark Weber:
Finite Models in FOL-Based Crypto-Protocol Verification. ARSPA-WITS 2009: 155-172 - 2008
- [b1]Tjark Weber:
SAT-based finite model generation for higher-order logic. Technical University Munich, Germany, 2008, pp. 1-141 - [c6]Hendrik Tews, Tjark Weber, Marcus Völp
A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code. SSV 2008: 79-96 - 2005
- [c5]Annabelle McIver
Towards Automated Proof Support for Probabilistic Distributed Systems. LPAR 2005: 534-548 - [c4]Tjark Weber:
Integrating a SAT Solver with an LCF-style Theorem Prover. PDPAR@CAV 2005: 67-78 - 2004
- [c3]Tjark Weber:
Towards Mechanized Program Verification with Separation Logic. CSL 2004: 250-264 - [c2]Tjark Weber:
Bounded Model Generation for Isabelle/HOL. D/PDPAR@IJCAR 2004: 103-116 - 2003
- [c1]Tjark Weber, James L. Caldwell
Constructively Characterizing Fold and Unfold. LOPSTR 2003: 110-127
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-25 05:58 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: