Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Tjark Weber
@article{DBLP:journals/afp/BergstromW24,
author = {Axel Bergstr{\"{o}}m and
Tjark Weber},
title = {Verified {QBF} Solving},
journal = {Arch. Formal Proofs},
volume = {2024},
year = {2024},
url = {https://www.isa-afp.org/entries/QBF\_Solver\_Verification.html},
timestamp = {Thu, 21 Mar 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/afp/BergstromW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/TorstenssonW23,
author = {Olle Torstensson and
Tjark Weber},
editor = {Uli Sattler and
Martin Suda},
title = {Hammering Floating-Point Arithmetic},
booktitle = {Frontiers of Combining Systems - 14th International Symposium, FroCoS
2023, Prague, Czech Republic, September 20-22, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14279},
pages = {217--235},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43369-6\_12},
doi = {10.1007/978-3-031-43369-6\_12},
timestamp = {Wed, 01 Nov 2023 08:59:02 +0100},
biburl = {https://dblp.org/rec/conf/frocos/TorstenssonW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lmcs/ParrowBEGW21,
author = {Joachim Parrow and
Johannes Borgstr{\"{o}}m and
Lars{-}Henrik Eriksson and
Ramunas Gutkovas and
Tjark Weber},
title = {Modal Logics for Nominal Transition Systems},
journal = {Log. Methods Comput. Sci.},
volume = {17},
number = {1},
year = {2021},
url = {https://lmcs.episciences.org/7137},
timestamp = {Mon, 08 Mar 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/lmcs/ParrowBEGW21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/smt/2020,
editor = {Fran{\c{c}}ois Bobot and
Tjark Weber},
title = {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},
series = {{CEUR} Workshop Proceedings},
volume = {2854},
publisher = {CEUR-WS.org},
year = {2021},
url = {https://ceur-ws.org/Vol-2854},
urn = {urn:nbn:de:0074-2854-1},
timestamp = {Fri, 10 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/smt/2020.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ictac/GengelbachW20,
author = {Arve Gengelbach and
Tjark Weber},
editor = {Violet Ka I Pun and
Volker Stolz and
Adenilso Sim{\~{a}}o},
title = {Proof-Theoretic Conservative Extension of {HOL} with Ad-hoc Overloading},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2020 - 17th International
Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12545},
pages = {23--42},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-64276-1\_2},
doi = {10.1007/978-3-030-64276-1\_2},
timestamp = {Tue, 01 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ictac/GengelbachW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2101-03807,
author = {Arve Gengelbach and
Johannes {\AA}man Pohjola and
Tjark Weber},
editor = {Claudio Sacerdoti Coen and
Alwen Tiu},
title = {Mechanisation of Model-theoretic Conservative Extension for {HOL}
with Ad-hoc Overloading},
booktitle = {Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages:
Theory and Practice, {LFMTP} 2020, Paris, France, 29th June 2020},
series = {{EPTCS}},
volume = {332},
pages = {1--17},
year = {2020},
url = {https://doi.org/10.4204/EPTCS.332.1},
doi = {10.4204/EPTCS.332.1},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2101-03807.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsat/WeberCDHNR19,
author = {Tjark Weber and
Sylvain Conchon and
David D{\'{e}}harbe and
Matthias Heizmann and
Aina Niemetz and
Giles Reger},
title = {The {SMT} Competition 2015-2018},
journal = {J. Satisf. Boolean Model. Comput.},
volume = {11},
number = {1},
pages = {221--259},
year = {2019},
url = {https://doi.org/10.3233/SAT190123},
doi = {10.3233/SAT190123},
timestamp = {Wed, 26 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jsat/WeberCDHNR19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/BartocciBBFGHHK19,
author = {Ezio Bartocci and
Dirk Beyer and
Paul E. Black and
Grigory Fedyukovich and
Hubert Garavel and
Arnd Hartmanns and
Marieke Huisman and
Fabrice Kordon and
Julian Nagele and
Mihaela Sighireanu and
Bernhard Steffen and
Martin Suda and
Geoff Sutcliffe and
Tjark Weber and
Akihisa Yamada},
editor = {Dirk Beyer and
Marieke Huisman and
Fabrice Kordon and
Bernhard Steffen},
title = {TOOLympics 2019: An Overview of Competitions in Formal Methods},
booktitle = {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}},
series = {Lecture Notes in Computer Science},
volume = {11429},
pages = {3--24},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-17502-3\_1},
doi = {10.1007/978-3-030-17502-3\_1},
timestamp = {Fri, 09 Apr 2021 18:45:37 +0200},
biburl = {https://dblp.org/rec/conf/tacas/BartocciBBFGHHK19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1904-02564,
author = {Joachim Parrow and
Johannes Borgstr{\"{o}}m and
Lars{-}Henrik Eriksson and
Ramunas Gutkovas and
Tjark Weber},
title = {Modal Logics for Nominal Transition Systems},
journal = {CoRR},
volume = {abs/1904.02564},
year = {2019},
url = {http://arxiv.org/abs/1904.02564},
eprinttype = {arXiv},
eprint = {1904.02564},
timestamp = {Wed, 24 Apr 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1904-02564.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/forte/ParrowWBE17,
author = {Joachim Parrow and
Tjark Weber and
Johannes Borgstr{\"{o}}m and
Lars{-}Henrik Eriksson},
editor = {Ahmed Bouajjani and
Alexandra Silva},
title = {Weak Nominal Modal Logic},
booktitle = {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{\^{a}}tel, Switzerland,
June 19-22, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10321},
pages = {179--193},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-60225-7\_13},
doi = {10.1007/978-3-319-60225-7\_13},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/forte/ParrowWBE17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/GengelbachW18,
author = {Arve Gengelbach and
Tjark Weber},
editor = {Sandra Alves and
Renata Wasserman},
title = {Model-Theoretic Conservative Extension for Definitional Theories},
booktitle = {12th Workshop on Logical and Semantic Frameworks, with Applications,
{LSFA} 2017, Bras{\'{\i}}lia, Brazil, September 23-24, 2017},
series = {Electronic Notes in Theoretical Computer Science},
volume = {338},
pages = {133--145},
publisher = {Elsevier},
year = {2017},
url = {https://doi.org/10.1016/j.entcs.2018.10.009},
doi = {10.1016/J.ENTCS.2018.10.009},
timestamp = {Tue, 16 Aug 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/entcs/GengelbachW18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/GomesGHSW16,
author = {Victor B. F. Gomes and
Walter Guttmann and
Peter H{\"{o}}fner and
Georg Struth and
Tjark Weber},
title = {Kleene Algebras with Domain},
journal = {Arch. Formal Proofs},
volume = {2016},
year = {2016},
url = {https://www.isa-afp.org/entries/KAD.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/GomesGHSW16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/WeberEPBG16,
author = {Tjark Weber and
Lars{-}Henrik Eriksson and
Joachim Parrow and
Johannes Borgstr{\"{o}}m and
Ramunas Gutkovas},
title = {Modal Logics for Nominal Transition Systems},
journal = {Arch. Formal Proofs},
volume = {2016},
year = {2016},
url = {https://www.isa-afp.org/entries/Modal\_Logics\_for\_NTS.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/WeberEPBG16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/ParrowW16,
author = {Joachim Parrow and
Tjark Weber},
title = {The Largest Respectful Function},
journal = {Log. Methods Comput. Sci.},
volume = {12},
number = {2},
year = {2016},
url = {https://doi.org/10.2168/LMCS-12(2:11)2016},
doi = {10.2168/LMCS-12(2:11)2016},
timestamp = {Thu, 25 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/ParrowW16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BengtsonPW16,
author = {Jesper Bengtson and
Joachim Parrow and
Tjark Weber},
title = {Psi-Calculi in Isabelle},
journal = {J. Autom. Reason.},
volume = {56},
number = {1},
pages = {1--47},
year = {2016},
url = {https://doi.org/10.1007/s10817-015-9336-2},
doi = {10.1007/S10817-015-9336-2},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BengtsonPW16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Weber16,
author = {Tjark Weber},
editor = {Tim King and
Ruzica Piskac},
title = {Scrambling and Descrambling {SMT-LIB} Benchmarks},
booktitle = {Proceedings of the 14th International Workshop on Satisfiability Modulo
Theories affiliated with the International Joint Conference on Automated
Reasoning, SMT@IJCAR 2016, Coimbra, Portugal, July 1-2, 2016},
series = {{CEUR} Workshop Proceedings},
volume = {1617},
pages = {31--40},
publisher = {CEUR-WS.org},
year = {2016},
url = {https://ceur-ws.org/Vol-1617/paper3.pdf},
timestamp = {Fri, 10 Mar 2023 16:23:14 +0100},
biburl = {https://dblp.org/rec/conf/cade/Weber16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/CokSW15,
author = {David R. Cok and
Aaron Stump and
Tjark Weber},
title = {The 2013 Evaluation of {SMT-COMP} and {SMT-LIB}},
journal = {J. Autom. Reason.},
volume = {55},
number = {1},
pages = {61--90},
year = {2015},
url = {https://doi.org/10.1007/s10817-015-9328-2},
doi = {10.1007/S10817-015-9328-2},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/CokSW15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/concur/ParrowBEGW15,
author = {Joachim Parrow and
Johannes Borgstr{\"{o}}m and
Lars{-}Henrik Eriksson and
Ramunas Gutkovas and
Tjark Weber},
editor = {Luca Aceto and
David de Frutos{-}Escrig},
title = {Modal Logics for Nominal Transition Systems},
booktitle = {26th International Conference on Concurrency Theory, {CONCUR} 2015,
Madrid, Spain, September 1.4, 2015},
series = {LIPIcs},
volume = {42},
pages = {198--211},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2015},
url = {https://doi.org/10.4230/LIPIcs.CONCUR.2015.198},
doi = {10.4230/LIPICS.CONCUR.2015.198},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/concur/ParrowBEGW15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/StruthW14,
author = {Georg Struth and
Tjark Weber},
title = {Relation Algebra},
journal = {Arch. Formal Proofs},
volume = {2014},
year = {2014},
url = {https://www.isa-afp.org/entries/Relation\_Algebra.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/StruthW14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jlp/ArmstrongSW14,
author = {Alasdair Armstrong and
Georg Struth and
Tjark Weber},
title = {Programming and automating mathematics in the Tarski-Kleene hierarchy},
journal = {J. Log. Algebraic Methods Program.},
volume = {83},
number = {2},
pages = {87--102},
year = {2014},
url = {https://doi.org/10.1016/j.jlap.2014.02.001},
doi = {10.1016/J.JLAP.2014.02.001},
timestamp = {Tue, 16 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jlp/ArmstrongSW14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsat/CokDW14,
author = {David R. Cok and
David D{\'{e}}harbe and
Tjark Weber},
title = {The 2014 {SMT} Competition},
journal = {J. Satisf. Boolean Model. Comput.},
volume = {9},
number = {1},
pages = {207--242},
year = {2014},
url = {https://doi.org/10.3233/sat190109},
doi = {10.3233/SAT190109},
timestamp = {Mon, 17 Aug 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsat/CokDW14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/ArmstrongSW13,
author = {Alasdair Armstrong and
Georg Struth and
Tjark Weber},
title = {Kleene Algebra},
journal = {Arch. Formal Proofs},
volume = {2013},
year = {2013},
url = {https://www.isa-afp.org/entries/Kleene\_Algebra.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/ArmstrongSW13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/ArmstrongSW13,
author = {Alasdair Armstrong and
Georg Struth and
Tjark Weber},
editor = {Sandrine Blazy and
Christine Paulin{-}Mohring and
David Pichardie},
title = {Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL},
booktitle = {Interactive Theorem Proving - 4th International Conference, {ITP}
2013, Rennes, France, July 22-26, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7998},
pages = {197--212},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39634-2\_16},
doi = {10.1007/978-3-642-39634-2\_16},
timestamp = {Wed, 25 Sep 2019 18:17:56 +0200},
biburl = {https://dblp.org/rec/conf/itp/ArmstrongSW13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1211-6190,
author = {Hendrik Tews and
Marcus V{\"{o}}lp and
Tjark Weber},
editor = {Franck Cassez and
Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
title = {On the Use of Underspecified Data-Type Semantics for Type Safety in
Low-Level Code},
booktitle = {Proceedings Seventh Conference on Systems Software Verification, {SSV}
2012, Sydney, Australia, 28-30 November 2012},
series = {{EPTCS}},
volume = {102},
pages = {73--87},
year = {2012},
url = {https://doi.org/10.4204/EPTCS.102.8},
doi = {10.4204/EPTCS.102.8},
timestamp = {Sun, 25 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1211-6190.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/pxtp/2012,
editor = {David Pichardie and
Tjark Weber},
title = {Proceedings of the Second International Workshop on Proof Exchange
for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012},
series = {{CEUR} Workshop Proceedings},
volume = {878},
publisher = {CEUR-WS.org},
year = {2012},
url = {https://ceur-ws.org/Vol-878},
timestamp = {Fri, 10 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/pxtp/2012.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sttt/Weber11,
author = {Tjark Weber},
title = {{SMT} solvers: new oracles for the {HOL} theorem prover},
journal = {Int. J. Softw. Tools Technol. Transf.},
volume = {13},
number = {5},
pages = {419--429},
year = {2011},
url = {https://doi.org/10.1007/s10009-011-0188-8},
doi = {10.1007/S10009-011-0188-8},
timestamp = {Thu, 02 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sttt/Weber11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/RelMiCS/FosterSW11,
author = {Simon Foster and
Georg Struth and
Tjark Weber},
editor = {Harrie C. M. de Swart},
title = {Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
- (Invited Tutorial)},
booktitle = {Relational and Algebraic Methods in Computer Science - 12th International
Conference, {RAMICS} 2011, Rotterdam, The Netherlands, May 30 - June
3, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6663},
pages = {52--67},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-21070-9\_5},
doi = {10.1007/978-3-642-21070-9\_5},
timestamp = {Wed, 15 Dec 2021 11:04:20 +0100},
biburl = {https://dblp.org/rec/conf/RelMiCS/FosterSW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ate/GuttmannSW11,
author = {Walter Guttmann and
Georg Struth and
Tjark Weber},
editor = {Peter H{\"{o}}fner and
Annabelle McIver and
Georg Struth},
title = {A Repository for Tarski-Kleene Algebras},
booktitle = {Proceedings of the First Workshop on Automated Theory Engineering,
Wroc{\l}aw, Poland, July 31, 2011},
series = {{CEUR} Workshop Proceedings},
volume = {760},
pages = {30--39},
publisher = {CEUR-WS.org},
year = {2011},
url = {https://ceur-ws.org/Vol-760/paper5.pdf},
timestamp = {Fri, 10 Mar 2023 16:23:01 +0100},
biburl = {https://dblp.org/rec/conf/ate/GuttmannSW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BohmeFSW11,
author = {Sascha B{\"{o}}hme and
Anthony C. J. Fox and
Thomas Sewell and
Tjark Weber},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Reconstruction of Z3's Bit-Vector Proofs in {HOL4} and Isabelle/HOL},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {183--198},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_15},
doi = {10.1007/978-3-642-25379-9\_15},
timestamp = {Thu, 14 Oct 2021 10:14:33 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BohmeFSW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfem/GuttmannSW11,
author = {Walter Guttmann and
Georg Struth and
Tjark Weber},
editor = {Shengchao Qin and
Zongyan Qiu},
title = {Automating Algebraic Methods in Isabelle},
booktitle = {Formal Methods and Software Engineering - 13th International Conference
on Formal Engineering Methods, {ICFEM} 2011, Durham, UK, October 26-28,
2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6991},
pages = {617--632},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-24559-6\_41},
doi = {10.1007/978-3-642-24559-6\_41},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/icfem/GuttmannSW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/KumarW11,
author = {Ramana Kumar and
Tjark Weber},
editor = {Marko C. J. D. van Eekelen and
Herman Geuvers and
Julien Schmaltz and
Freek Wiedijk},
title = {Validating {QBF} Validity in {HOL4}},
booktitle = {Interactive Theorem Proving - Second International Conference, {ITP}
2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6898},
pages = {168--183},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22863-6\_14},
doi = {10.1007/978-3-642-22863-6\_14},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/KumarW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/BattyOSSW11,
author = {Mark Batty and
Scott Owens and
Susmit Sarkar and
Peter Sewell and
Tjark Weber},
editor = {Thomas Ball and
Mooly Sagiv},
title = {Mathematizing {C++} concurrency},
booktitle = {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},
publisher = {{ACM}},
year = {2011},
url = {https://doi.org/10.1145/1926385.1926394},
doi = {10.1145/1926385.1926394},
timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},
biburl = {https://dblp.org/rec/conf/popl/BattyOSSW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ppdp/BlanchetteWBOS11,
author = {Jasmin Christian Blanchette and
Tjark Weber and
Mark Batty and
Scott Owens and
Susmit Sarkar},
editor = {Peter Schneider{-}Kamp and
Michael Hanus},
title = {Nitpicking {C++} concurrency},
booktitle = {Proceedings of the 13th International {ACM} {SIGPLAN} Conference on
Principles and Practice of Declarative Programming, July 20-22, 2011,
Odense, Denmark},
pages = {113--124},
publisher = {{ACM}},
year = {2011},
url = {https://doi.org/10.1145/2003476.2003493},
doi = {10.1145/2003476.2003493},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ppdp/BlanchetteWBOS11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pxtp/BohmeW11,
author = {Sascha B{\"{o}}hme and
Tjark Weber},
editor = {Pascal Fontaine and
Aaron Stump},
title = {Designing Proof Formats: {A} User's Perspective},
booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem
Proving, Wroc{\l}aw, Poland, August 1, 2011},
pages = {27--32},
year = {2011},
url = {https://pxtp2011.loria.fr/PxTP2011.pdf\#page=31},
timestamp = {Thu, 25 Nov 2021 17:51:05 +0100},
biburl = {https://dblp.org/rec/conf/pxtp/BohmeW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BohmeW10,
author = {Sascha B{\"{o}}hme and
Tjark Weber},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {Fast LCF-Style Proof Reconstruction for {Z3}},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {179--194},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_14},
doi = {10.1007/978-3-642-14052-5\_14},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/BohmeW10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Weber10,
author = {Tjark Weber},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {Validating {QBF} Invalidity in {HOL4}},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {466--480},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_32},
doi = {10.1007/978-3-642-14052-5\_32},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/Weber10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/japll/WeberA09,
author = {Tjark Weber and
Hasan Amjad},
title = {Efficiently checking propositional refutations in {HOL} theorem provers},
journal = {J. Appl. Log.},
volume = {7},
number = {1},
pages = {26--40},
year = {2009},
url = {https://doi.org/10.1016/j.jal.2007.07.003},
doi = {10.1016/J.JAL.2007.07.003},
timestamp = {Tue, 16 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/japll/WeberA09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/TewsVW09,
author = {Hendrik Tews and
Marcus V{\"{o}}lp and
Tjark Weber},
title = {Formal Memory Models for the Verification of Low-Level Operating-System
Code},
journal = {J. Autom. Reason.},
volume = {42},
number = {2-4},
pages = {189--227},
year = {2009},
url = {https://doi.org/10.1007/s10817-009-9122-0},
doi = {10.1007/S10817-009-9122-0},
timestamp = {Sun, 25 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/TewsVW09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ifip1-7/JurjensW09,
author = {Jan J{\"{u}}rjens and
Tjark Weber},
editor = {Pierpaolo Degano and
Luca Vigan{\`{o}}},
title = {Finite Models in FOL-Based Crypto-Protocol Verification},
booktitle = {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},
series = {Lecture Notes in Computer Science},
volume = {5511},
pages = {155--172},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03459-6\_11},
doi = {10.1007/978-3-642-03459-6\_11},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/ifip1-7/JurjensW09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{DBLP:phd/de/Weber2008,
author = {Tjark Weber},
title = {SAT-based finite model generation for higher-order logic},
school = {Technical University Munich, Germany},
year = {2008},
url = {http://mediatum2.ub.tum.de/doc/676608/document.pdf},
urn = {urn:nbn:de:bvb:91-diss-20081018-676608-1-8},
timestamp = {Sat, 17 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/phd/de/Weber2008.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/TewsWV08,
author = {Hendrik Tews and
Tjark Weber and
Marcus V{\"{o}}lp},
editor = {Ralf Huuck and
Gerwin Klein and
Bastian Schlich},
title = {A Formal Model of Memory Peculiarities for the Verification of Low-Level
Operating-System Code},
booktitle = {Proceedings of the 3rd International Workshop on Systems Software
Verification, {SSV} 2008, Sydney, Australia, February 25-27, 2008},
series = {Electronic Notes in Theoretical Computer Science},
volume = {217},
pages = {79--96},
publisher = {Elsevier},
year = {2008},
url = {https://doi.org/10.1016/j.entcs.2008.06.043},
doi = {10.1016/J.ENTCS.2008.06.043},
timestamp = {Fri, 17 Feb 2023 10:34:05 +0100},
biburl = {https://dblp.org/rec/journals/entcs/TewsWV08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/McIverW05,
author = {Annabelle McIver and
Tjark Weber},
editor = {Geoff Sutcliffe and
Andrei Voronkov},
title = {Towards Automated Proof Support for Probabilistic Distributed Systems},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 12th
International Conference, {LPAR} 2005, Montego Bay, Jamaica, December
2-6, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3835},
pages = {534--548},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11591191\_37},
doi = {10.1007/11591191\_37},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/lpar/McIverW05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/Weber06,
author = {Tjark Weber},
editor = {Alessandro Armando and
Alessandro Cimatti},
title = {Integrating a {SAT} Solver with an LCF-style Theorem Prover},
booktitle = {Proceedings of the Third Workshop on Pragmatics of Decision Procedures
in Automated Reasoning, PDPAR@CAV 2005, Edinburgh, UK, July 12, 2005},
series = {Electronic Notes in Theoretical Computer Science},
volume = {144},
number = {2},
pages = {67--78},
publisher = {Elsevier},
year = {2005},
url = {https://doi.org/10.1016/j.entcs.2005.12.007},
doi = {10.1016/J.ENTCS.2005.12.007},
timestamp = {Fri, 16 Dec 2022 10:24:43 +0100},
biburl = {https://dblp.org/rec/journals/entcs/Weber06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/Weber04,
author = {Tjark Weber},
editor = {Jerzy Marcinkowski and
Andrzej Tarlecki},
title = {Towards Mechanized Program Verification with Separation Logic},
booktitle = {Computer Science Logic, 18th International Workshop, {CSL} 2004, 13th
Annual Conference of the EACSL, Karpacz, Poland, September 20-24,
2004, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3210},
pages = {250--264},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/978-3-540-30124-0\_21},
doi = {10.1007/978-3-540-30124-0\_21},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/csl/Weber04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/Weber05,
author = {Tjark Weber},
editor = {Wolfgang Ahrendt and
Peter Baumgartner and
Hans de Nivelle and
Silvio Ranise and
Cesare Tinelli},
title = {Bounded Model Generation for Isabelle/HOL},
booktitle = {Selected Papers from the Workshops on Disproving, D@IJCAR 2004, and
the Second International Workshop on Pragmatics of Decision Procedures,
PDPAR@IJCAR 2004, Cork, Ireland, July 2004},
series = {Electronic Notes in Theoretical Computer Science},
volume = {125},
number = {3},
pages = {103--116},
publisher = {Elsevier},
year = {2004},
url = {https://doi.org/10.1016/j.entcs.2004.10.027},
doi = {10.1016/J.ENTCS.2004.10.027},
timestamp = {Tue, 13 Dec 2022 13:53:40 +0100},
biburl = {https://dblp.org/rec/journals/entcs/Weber05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lopstr/WeberC03,
author = {Tjark Weber and
James L. Caldwell},
editor = {Maurice Bruynooghe},
title = {Constructively Characterizing Fold and Unfold},
booktitle = {Logic Based Program Synthesis and Transformation, 13th International
Symposium {LOPSTR} 2003, Uppsala, Sweden, August 25-27, 2003, Revised
Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {3018},
pages = {110--127},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/978-3-540-25938-1\_11},
doi = {10.1007/978-3-540-25938-1\_11},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lopstr/WeberC03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
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.
last updated on 2024-03-22 22:22 CET 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:
