Stop the war!
Остановите войну!
for scientists:
default search action
BibTeX 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} }
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.