Search

Your search keyword '"Hölzl, Johannes"' showing total 83 results
Start Over Author "Hölzl, Johannes"
83 results on '"Hölzl, Johannes"'

1. Formalizing the Solution to the Cap Set Problem

Author

Dahmen, Sander R., Hölzl, Johannes, and Lewis, Robert Y.

Subjects
Computer Science - Logic in Computer Science, Mathematics - Combinatorics
Abstract

In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $\mathbb{F}^n_q$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q = 3$, where it is commonly known as the \emph{cap set problem}. Ellenberg and Gijswijt's proof was published in the \emph{Annals of Mathematics} and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in $\mathbb{F}^n_q$ and concrete values for the case $q = 3$. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants., Comment: To appear in proceedings of Interactive Theorem Proving (ITP) 2019

Published
2019

3. A Verified Compiler for Probability Density Functions

Author

Eberl, Manuel, Hölzl, Johannes, and Nipkow, Tobias

Subjects
Computer Science - Programming Languages, Computer Science - Logic in Computer Science, Mathematics - Probability
Abstract

Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a simple probabilistic functional language. In this work, we implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a formal proof of its soundness w.r.t. the semantics of the source and target language. Together with Isabelle's code generation for inductive predicates, this yields a fully verified, executable density compiler. The proof is done in two steps, using a standard refinement approach: first, an abstract compiler working with abstract functions modelled directly in the theorem prover's logic is defined and proven sound. Then, this compiler is refined to a concrete version that returns a target-language expression., Comment: Presented at ESOP 2015

Published
2017
Full Text
View/download PDF

4. A formally verified proof of the Central Limit Theorem

Author

Avigad, Jeremy, Hölzl, Johannes, and Serafin, Luke

Subjects
Computer Science - Mathematical Software, Computer Science - Logic in Computer Science, Mathematics - Probability, 60F05, 03B35, F.4.1, G.3
Abstract

We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle's libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. We also discuss the libraries and infrastructure that supported the formalization, and reflect on some of the lessons we have learned from the effort.

Published
2014

5. Interactive verification of Markov chains: Two distributed protocol case studies

Author

Hölzl, Johannes and Nipkow, Tobias

Subjects
Computer Science - Logic in Computer Science
Abstract

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 interactive proof assistant Isabelle/HOL. The first case study is a detailed description of how we verified properties of the ZeroConf protocol, a decentral address allocation protocol. The second case study shows the more involved verification of anonymity properties of the Crowds protocol, an anonymizing protocol., Comment: In Proceedings QFM 2012, arXiv:1212.3454

Published
2012
Full Text
View/download PDF

6. MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)

Author

Wimmer, Simon, Hölzl, Johannes, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Avigad, Jeremy, editor, and Mahboubi, Assia, editor

Published
2018
Full Text
View/download PDF

7. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Author

Biendarra, Julian, Blanchette, Jasmin Christian, Bouzy, Aymeric, Desharnais, Martin, Fleury, Mathias, Hölzl, Johannes, Kunčar, Ondřej, Lochbihler, Andreas, Meier, Fabian, Panny, Lorenz, Popescu, Andrei, Sternagel, Christian, Thiemann, René, Traytel, Dmitriy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Dixon, Clare, editor, and Finger, Marcelo, editor

Published
2017
Full Text
View/download PDF

8. Formalising Semantics for Expected Running Time of Probabilistic Programs

Author

Hölzl, Johannes, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Blanchette, Jasmin Christian, editor, and Merz, Stephan, editor

Published
2016
Full Text
View/download PDF

9. A Formalized Hierarchy of Probabilistic System Types : Proof Pearl

Author

Hölzl, Johannes, Lochbihler, Andreas, Traytel, Dmitriy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Urban, Christian, editor, and Zhang, Xingyuan, editor

Published
2015
Full Text
View/download PDF

11. Truly Modular (Co)datatypes for Isabelle/HOL

Author

Blanchette, Jasmin Christian, Hölzl, Johannes, Lochbihler, Andreas, Panny, Lorenz, Popescu, Andrei, Traytel, Dmitriy, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Kobsa, Alfred, editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Weikum, Gerhard, editor, Klein, Gerwin, editor, and Gamboa, Ruben, editor

Published
2014
Full Text
View/download PDF

12. Recursive Functions on Lazy Lists via Domains and Topologies

Author

Lochbihler, Andreas, Hölzl, Johannes, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Kobsa, Alfred, editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Weikum, Gerhard, editor, Klein, Gerwin, editor, and Gamboa, Ruben, editor

Published
2014
Full Text
View/download PDF

13. Noninterfering Schedulers : When Possibilistic Noninterference Implies Probabilistic Noninterference

Author

Popescu, Andrei, Hölzl, Johannes, Nipkow, Tobias, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Heckel, Reiko, editor, and Milius, Stefan, editor

Published
2013
Full Text
View/download PDF

14. Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

Author

Hölzl, Johannes, Immler, Fabian, Huffman, Brian, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Blazy, Sandrine, editor, Paulin-Mohring, Christine, editor, and Pichardie, David, editor

Published
2013
Full Text
View/download PDF

15. Formalizing Probabilistic Noninterference

Author

Popescu, Andrei, Hölzl, Johannes, Nipkow, Tobias, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Gonthier, Georges, editor, and Norrish, Michael, editor

Published
2013
Full Text
View/download PDF

16. Proving Concurrent Noninterference

Author

Popescu, Andrei, Hölzl, Johannes, Nipkow, Tobias, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Hawblitzel, Chris, editor, and Miller, Dale, editor

Published
2012
Full Text
View/download PDF

17. Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL

Author

Immler, Fabian, Hölzl, Johannes, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Beringer, Lennart, editor, and Felty, Amy, editor

Published
2012
Full Text
View/download PDF

18. Verifying pCTL Model Checking

Author

Hölzl, Johannes, Nipkow, Tobias, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Flanagan, Cormac, editor, and König, Barbara, editor

Published
2012
Full Text
View/download PDF

19. Three Chapters of Measure Theory in Isabelle/HOL

Author

Hölzl, Johannes, Heller, Armin, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, van Eekelen, Marko, editor, Geuvers, Herman, editor, Schmaltz, Julien, editor, and Wiedijk, Freek, editor

Published
2011
Full Text
View/download PDF

22. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Author

Biendarra, Julian, primary, Blanchette, Jasmin Christian, additional, Bouzy, Aymeric, additional, Desharnais, Martin, additional, Fleury, Mathias, additional, Hölzl, Johannes, additional, Kunčar, Ondřej, additional, Lochbihler, Andreas, additional, Meier, Fabian, additional, Panny, Lorenz, additional, Popescu, Andrei, additional, Sternagel, Christian, additional, Thiemann, René, additional, and Traytel, Dmitriy, additional

Published
2017
Full Text
View/download PDF

38. Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic

Author

Hölzl, Johannes, Nipkow, Tobias (Prof., Ph.D.), and Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.)

Subjects
Informatik, Interactive Theorem Proving, Probability Theory, Markov Chains, ddc:004, Interaktives Theorembeweisen, Wahrscheinlichkeitstheorie, Markov-Ketten
Abstract

The goal of this work is the verification of probabilistic systems in the interactive theorem prover Isabelle/HOL. This requires the formalization of probability theory. We construct probability spaces with infinitely many independent random variables and the stochastic process of a Markov chain. We use these probability spaces to verify the correctness of probabilistic model checking and to verify properties of the ZeroConf protocol and the Crowds protocol. Ziel dieser Arbeit ist die Verifikation probabilistischer Systeme in dem interaktiven Theorembeweiser Isabelle/HOL. Dies setzt die Formalisierung von Wahrscheinlichkeitstheorie voraus. Wir konstruieren W-Räume mit unendlich vielen, unabhängigen Zufallsvariablen und den zu einer Markov-Kette gehörenden stochastischen Prozess. Wir verwenden diese W-Räume um die Korrektheit von probabilistischem Model Checking und Eigenschaften des ZeroConf-Protokolls und des Crowds-Protokoll zu verifizieren.

Published
2013

39. Entwicklungstendenzen im österreichischen Wettkampfbodybuilding

Author

Hölzl, Johannes

Abstract

The objective of this master thesis is to take an in dept look at the sociological approach of sport sciences to the development of bodybuilding, with a focus on bodybuilding as competitive sport in austria. Luhmann’s Systemtheory (1984) is used as a basis to study bodybuilding as a functional differentiated (?) system of sports. Additionally experts on the sport were interviewed. Through this approach it is possible to point out relevant developments in the scoiety, as well as the organization and interaction in bodybuilding. The impact of trends such as erotizisation, individualization, technization, tendencies of extremism and globalization on bodybuilding is demonstrated. Further research focuses were the differentiation of the sport, demographic development, the topic of doping abuse as well as structural linking., Ziel der Arbeit ist es, das Phänomen der Entwicklung der Sportart Bodybuilding, fokussiert auf den österreichischen Leistungssport, aus sportsoziologischer Perspektive zu betrachten. Bodybuilding wird dabei anhand der Luhmannschen Systemtheorie (1984) als funktional differenziertes Sportartensystem betrachtet und mithilfe von Experteninterviews untersucht. Relevante Entwicklungen in der Gesellschaft, sowie der Organisation und Interaktion im Bodybuildingsport können so aufgezeigt werden. Die Trends der Erotisierung, Individualisierung, Technisierung, Extremisierung und Globalisierung werden in ihren Auswirkungen im Bodybuilding nachgewiesen und systemtheoretische Zusammenhänge in der Entwicklung der Sportart aufgezeigt. Die Ausdifferenzierung der Sportart, Demografische Entwicklung, Umgang mit der Dopingthematik und strukturelle Kopplung sind weitere Forschungsschwerpunkte.

Published
2012
Full Text
View/download PDF

42. Truly Modular (Co)datatypes for Isabelle/HOL

Author

Klein, Gerwin, Gamboa, Ruben, Blanchette, Jasmin Christian, Hölzl, Johannes, Lochbihler, Andreas, Panny, Lorenz, Popescu, Andrei, Traytel, Dmitriy, Klein, Gerwin, Gamboa, Ruben, Blanchette, Jasmin Christian, Hölzl, Johannes, Lochbihler, Andreas, Panny, Lorenz, Popescu, Andrei, and Traytel, Dmitriy

Published
2014

43. Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic

Author

Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.), Nipkow, Tobias (Prof., Ph.D.), Hölzl, Johannes, Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.), Nipkow, Tobias (Prof., Ph.D.), and Hölzl, Johannes

Abstract

The goal of this work is the verification of probabilistic systems in the interactive theorem prover Isabelle/HOL. This requires the formalization of probability theory. We construct probability spaces with infinitely many independent random variables and the stochastic process of a Markov chain. We use these probability spaces to verify the correctness of probabilistic model checking and to verify properties of the ZeroConf protocol and the Crowds protocol., Ziel dieser Arbeit ist die Verifikation probabilistischer Systeme in dem interaktiven Theorembeweiser Isabelle/HOL. Dies setzt die Formalisierung von Wahrscheinlichkeitstheorie voraus. Wir konstruieren W-Räume mit unendlich vielen, unabhängigen Zufallsvariablen und den zu einer Markov-Kette gehörenden stochastischen Prozess. Wir verwenden diese W-Räume um die Korrektheit von probabilistischem Model Checking und Eigenschaften des ZeroConf-Protokolls und des Crowds-Protokoll zu verifizieren.

Published
2013

44. Formal Verification of Language-Based Concurrent Noninterference

Author

Popescu, Andrei, Hölzl, Johannes, Nipkow, Tobias, Popescu, Andrei, Hölzl, Johannes, and Nipkow, Tobias

Abstract

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 literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.

Published
2013

45. Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic

Author

Nipkow, Tobias (Prof., Ph.D.), Nipkow, Tobias (Prof., Ph.D.);Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.), Hölzl, Johannes, Nipkow, Tobias (Prof., Ph.D.), Nipkow, Tobias (Prof., Ph.D.);Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.), and Hölzl, Johannes

Abstract

The goal of this work is the verification of probabilistic systems in the interactive theorem prover Isabelle/HOL. This requires the formalization of probability theory. We construct probability spaces with infinitely many independent random variables and the stochastic process of a Markov chain. We use these probability spaces to verify the correctness of probabilistic model checking and to verify properties of the ZeroConf protocol and the Crowds protocol., Ziel dieser Arbeit ist die Verifikation probabilistischer Systeme in dem interaktiven Theorembeweiser Isabelle/HOL. Dies setzt die Formalisierung von Wahrscheinlichkeitstheorie voraus. Wir konstruieren W-Räume mit unendlich vielen, unabhängigen Zufallsvariablen und den zu einer Markov-Kette gehörenden stochastischen Prozess. Wir verwenden diese W-Räume um die Korrektheit von probabilistischem Model Checking und Eigenschaften des ZeroConf-Protokolls und des Crowds-Protokoll zu verifizieren.

Published
2013

Catalog

Books, media, physical & digital resources
See catalog results