The following pages link to Tjark Weber (Q286783):
Displaying 24 items.
- The 2013 evaluation of SMT-COMP and SMT-LIB (Q286784) (← links)
- Programming and automating mathematics in the Tarski-Kleene hierarchy (Q406433) (← links)
- Formal memory models for the verification of low-level operating-system code (Q835773) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Proof-theoretic conservative extension of HOL with ad-hoc overloading (Q2037933) (← links)
- Model-theoretic conservative extension for definitional theories (Q2333319) (← links)
- (Q2848061) (← links)
- (Q2848690) (← links)
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL (Q3007567) (← links)
- Validating QBF Validity in HOL4 (Q3088005) (← links)
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212) (← links)
- Finite Models in FOL-Based Crypto-Protocol Verification (Q3184717) (← links)
- (Q3184993) (← links)
- Weak Nominal Modal Logic (Q5082196) (← links)
- Computer Science Logic (Q5311261) (← links)
- Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL (Q5327345) (← links)
- (Q5357704) (← links)
- Towards Automated Proof Support for Probabilistic Distributed Systems (Q5387864) (← links)
- Mathematizing C++ concurrency (Q5408531) (← links)
- The Largest Respectful Function (Q5739896) (← links)
- Fast LCF-Style Proof Reconstruction for Z3 (Q5747649) (← links)
- Validating QBF Invalidity in HOL4 (Q5747670) (← links)
- (Q5856409) (← links)
- Psi-calculi in Isabelle (Q5890661) (← links)
