Zobrazeno 1 - 10
of 213
pro vyhledávání: '"Tobias Nipkow"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 18, Issue 1 (2022)
We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balancing, and bin packing. We uncover incompletenesses in existing proofs an
Externí odkaz:
https://doaj.org/article/840dfb64b1a249ccb5dba0e51223a2fe
Autor:
THOMAS HALES, MARK ADAMS, GERTRUD BAUER, TAT DAT DANG, JOHN HARRISON, LE TRUONG HOANG, CEZARY KALISZYK, VICTOR MAGRON, SEAN MCLAUGHLIN, TAT THANG NGUYEN, QUANG TRUONG NGUYEN, TOBIAS NIPKOW, STEVEN OBUA, JOSEPH PLESO, JASON RUTE, ALEXEY SOLOVYEV, THI HOAI AN TA, NAM TRUNG TRAN, THI DIEP TRIEU, JOSEF URBAN, KY VU, ROLAND ZUMKELLER
Publikováno v:
Forum of Mathematics, Pi, Vol 5 (2017)
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
Externí odkaz:
https://doaj.org/article/0dae9a3d3e584c73a937daefc20afe3b
Publikováno v:
Journal of Formalized Reasoning, Vol 6, Iss 1, Pp 1-30 (2013)
We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of non-interference variants from the l
Externí odkaz:
https://doaj.org/article/f9f77bc6924a46f4bdbed8104421969c
Autor:
Johannes Hölzl, Tobias Nipkow
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 103, Iss Proc. QFM 2012, Pp 17-31 (2012)
Probabilistic model checkers like PRISM only check probabilistic systems of a fixed size. To guarantee the desired properties for an arbitrary size, mathematical analysis is necessary. We show for two case studies how this can be done in the interact
Externí odkaz:
https://doaj.org/article/06a27452d1e2405cb0af605d7340ec72
Autor:
Simon Roßkopf, Tobias Nipkow
Publikováno v:
Journal of Automated Reasoning. 67
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executabl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::95982e8f385bce8a6644ab9ed796b5e4
https://doi.org/10.1007/s10817-022-09648-w
https://doi.org/10.1007/s10817-022-09648-w
Publikováno v:
Journal of Automated Reasoning. 64:879-910
This work is a case study of the formal verification and complexity analysis of some famous probabilistic algorithms and data structures in the proof assistant Isabelle/HOL. In particular, we consider the expected number of comparisons in randomised
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::579381b7e0e2d94998c94b10575e5f0c
https://doi.org/10.1007/s10817-020-09545-0
https://doi.org/10.1007/s10817-020-09545-0
Autor:
Niels Mündler, Tobias Nipkow
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783031177149
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1a9ef3d0992b4944daa13332533864f7
https://doi.org/10.1007/978-3-031-17715-6_21
https://doi.org/10.1007/978-3-031-17715-6_21
Publikováno v:
Formal Aspects of Computing. 31:675-698
Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today's powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search, borrowing te
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8891d9db08ca9ea546c99b7729ce6f59
https://doi.org/10.1007/s00165-019-00492-1
https://doi.org/10.1007/s00165-019-00492-1
Autor:
Tobias Nipkow
Publikováno v:
CPP
We report on a new course Verified Functional Data Structures and Algorithms taught at the Technical University of Munich. The course first introduces students to interactive theorem proving with the Isabelle proof assistant. Then it covers a range o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5a4a46594672a1b0d7d4338f3aa790b4
https://doi.org/10.1145/3437992.3439910
https://doi.org/10.1145/3437992.3439910
Autor:
Tobias Nipkow, Simon Roßkopf
Publikováno v:
Automated Deduction – CADE 28 ISBN: 9783030798758
CADE
CADE
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executabl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::842ffcbfc1fc9944907c4d632b21b2e8
https://doi.org/10.1007/978-3-030-79876-5_6
https://doi.org/10.1007/978-3-030-79876-5_6