Foto von Tobias Nipkow

Scopus-Profil ansehen

Tobias Nipkow

Prof.

 https://orcid.org/0000-0003-0730-515X
1982 …2024

Publikationen pro Jahr

Suchergebnisse

  • 2024

    Alpha-Beta Pruning Verified

    Nipkow, T., Sept. 2024, 15th International Conference on Interactive Theorem Proving, ITP 2024. Bertot, Y., Kutsia, T. & Norrish, M. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1. (Leibniz International Proceedings in Informatics, LIPIcs; Band 309).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • A Note on Proofs of Earley’s Recognizer

    Nipkow, T. & Rau, M., 2024, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Science and Business Media Deutschland GmbH, S. 45-55 11 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band LNCS 14781).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Kapitel › Begutachtung

  • A Verified Earley Parser

    Rau, M. & Nipkow, T., Sept. 2024, 15th International Conference on Interactive Theorem Proving, ITP 2024. Bertot, Y., Kutsia, T. & Norrish, M. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 31. (Leibniz International Proceedings in Informatics, LIPIcs; Band 309).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • Gale-Shapley Verified

    Nipkow, T., Juni 2024, in: Journal of Automated Reasoning. 68, 2, 12.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access

  • Region Quadtrees Verified

    Nipkow, T., 2024, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Science and Business Media Deutschland GmbH, S. 243-254 12 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band LNCS 14660).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Kapitel › Begutachtung

  • 2023

    A Formalization and Proof Checker for Isabelle’s Metalogic

    Roßkopf, S. & Nipkow, T., März 2023, in: Journal of Automated Reasoning. 67, 1, 1.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access

  • Real-Time Double-Ended Queue Verified (Proof Pearl)

    Toth, B. & Nipkow, T., Juli 2023, 14th International Conference on Interactive Theorem Proving, ITP 2023. Naumowicz, A. & Thiemann, R. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 29. (Leibniz International Proceedings in Informatics, LIPIcs; Band 268).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • Verification of NP-Hardness Reduction Functions for Exact Lattice Problems

    Kreuzer, K. & Nipkow, T., 2023, Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. Pientka, B. & Tinelli, C. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 365-381 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 14132 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    2 Zitate (Scopus)
  • 2022

    A Verified Implementation of B + -Trees in Isabelle/HOL

    Mündler, N. & Nipkow, T., 2022, Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. Seidl, H., Liu, Z. & Pasareanu, C. S. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 324-341 18 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 13572 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access

  • VERIFIED APPROXIMATION ALGORITHMS

    Essmann, R., Nipkow, T., Robillard, S. & Sulejmani, U., 2022, in: Logical Methods in Computer Science. 18, 1, S. 36:1-36:21

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access
  • 2021

    A Verified Decision Procedure for Orders in Isabelle/HOL

    Stevens, L. & Nipkow, T., 2021, Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings. Hou, Z. & Ganesh, V. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 127-143 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12971 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)

  • Isabelle’s Metalogic: Formalization and Proof Checker

    Nipkow, T. & Roßkopf, S., 2021, Automated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings. Platzer, A. & Sutcliffe, G. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 93-110 18 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12699 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    9 Zitate (Scopus)

  • Teaching algorithms and data structures with a proof assistant (invited talk)

    Nipkow, T., 17 Jan. 2021, CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Hritcu, C. & Popescu, A. (Hrsg.). Association for Computing Machinery, Inc, S. 1-3 3 S. (CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    2 Zitate (Scopus)
  • 2020

    Proof pearl: Braun trees

    Nipkow, T. & Sewell, T., 20 Jan. 2020, CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020. Blanchette, J. & Hritcu, C. (Hrsg.). Association for Computing Machinery, Inc, S. 18-31 14 S. (CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)

  • Verification of Closest Pair of Points Algorithms

    Rau, M. & Nipkow, T., 2020, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings. Peltier, N. & Sofronie-Stokkermans, V. (Hrsg.). Springer, S. 341-357 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12167 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)

  • Verified Analysis of Random Binary Tree Structures

    Eberl, M., Haslbeck, M. W. & Nipkow, T., 1 Juni 2020, in: Journal of Automated Reasoning. 64, 5, S. 879-910 32 S.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access
    8 Zitate (Scopus)

  • Verified Approximation Algorithms

    Eßmann, R., Nipkow, T. & Robillard, S., 2020, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings. Peltier, N. & Sofronie-Stokkermans, V. (Hrsg.). Springer, S. 291-306 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12167 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    3 Zitate (Scopus)

  • Verified Textbook Algorithms: A Biased Survey

    Nipkow, T., Eberl, M. & Haslbeck, M. P. L., 2020, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. Hung, D. V. & Sokolsky, O. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 25-53 29 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12302 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    8 Zitate (Scopus)
  • 2019

    Amortized Complexity Verified

    Nipkow, T. & Brinkop, H., 15 März 2019, in: Journal of Automated Reasoning. 62, 3, S. 367-391 25 S.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    15 Zitate (Scopus)

  • From LCF to Isabelle/HOL

    Paulson, L. C., Nipkow, T. & Wenzel, M., 1 Dez. 2019, in: Formal Aspects of Computing. 31, 6, S. 675-698 24 S.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access
    37 Zitate (Scopus)

  • Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra

    Lammich, P. & Nipkow, T., Sept. 2019, 10th International Conference on Interactive Theorem Proving, ITP 2019. Harrison, J., O'Leary, J. & Tolmach, A. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 23. (Leibniz International Proceedings in Informatics, LIPIcs; Band 141).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    4 Zitate (Scopus)

  • Trustworthy graph algorithms

    Abdulaziz, M., Mehlhorn, K. & Nipkow, T., Aug. 2019, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019. Katoen, J.-P., Heggernes, P. & Rossmanith, P. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1. (Leibniz International Proceedings in Informatics, LIPIcs; Band 138).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    6 Zitate (Scopus)
  • 2018

    A verified compiler from isabelle/HOL to CakeML

    Hupel, L. & Nipkow, T., 2018, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Ahmed, A. (Hrsg.). Springer Verlag, S. 999-1026 28 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10801 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    29 Zitate (Scopus)

  • Hoare logics for time bounds: A study in meta theory

    Haslbeck, M. P. L. & Nipkow, T., 2018, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Beyer, D. & Huisman, M. (Hrsg.). Springer Verlag, S. 155-171 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10805 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    11 Zitate (Scopus)

  • Verified Analysis of Random Binary Tree Structures

    Eberl, M., Haslbeck, M. W. & Nipkow, T., 2018, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Avigad, J. & Mahboubi, A. (Hrsg.). Springer Verlag, S. 196-214 19 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10895 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    4 Zitate (Scopus)

  • Verified Memoization and Dynamic Programming

    Wimmer, S., Hu, S. & Nipkow, T., 2018, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Avigad, J. & Mahboubi, A. (Hrsg.). Springer Verlag, S. 579-596 18 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10895 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    5 Zitate (Scopus)
  • 2017

    A FORMAL PROOF of the KEPLER CONJECTURE

    Hales, T., Adams, M., Bauer, G., Dang, T. D., Harrison, J., Hoang, L. T., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T. T., Nguyen, Q. T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T. H. A., Tran, N. T., Trieu, T. D. & Urban, J. &2 mehr, Vu, K. & Zumkeller, R., 2017, in: Forum of Mathematics, Pi. 5, e2.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access
    255 Zitate (Scopus)

  • Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL

    Rizaldi, A., Keinholz, J., Huber, M., Feldle, J., Immler, F., Althoff, M., Hilgendorf, E. & Nipkow, T., 2017, Integrated Formal Methods - 13th International Conference, IFM 2017, Proceedings. Schneider, S. & Polikarpova, N. (Hrsg.). Springer Verlag, S. 50-66 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10510 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    67 Zitate (Scopus)

  • Formalized Proof Systems for Propositional Logic

    Michaelis, J. & Nipkow, T., 2017, 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Kaposi, A. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 5. (Leibniz International Proceedings in Informatics, LIPIcs; Band 104).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    13 Zitate (Scopus)

  • Verified root-balanced trees

    Nipkow, T., 2017, Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Proceedings. Chang, B.-Y. E. (Hrsg.). Springer Verlag, S. 255-272 18 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10695 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    9 Zitate (Scopus)
  • 2016

    Automatic functional correctness proofs for functional search trees

    Nipkow, T., 2016, Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Blanchette, J. C. & Merz, S. (Hrsg.). Springer Verlag, S. 307-322 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9807 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    10 Zitate (Scopus)

  • Verified Analysis of Functional Data Structures

    Nipkow, T., 1 Juni 2016, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. Kesner, D. & Pientka, B. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 4. (Leibniz International Proceedings in Informatics, LIPIcs; Band 52).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    2 Zitate (Scopus)

  • Verified analysis of list update algorithms

    Haslbeck, M. P. L. & Nipkow, T., 1 Dez. 2016, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016. Lal, A., Akshay, S., Saurabh, S., Sen, S. & Saurabh, S. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, S. 49.1-49.15 (Leibniz International Proceedings in Informatics, LIPIcs; Band 65).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)
  • 2015

    Amortized complexity verified

    Nipkow, T., 2015, Interactive Theorem Proving - 6th International Conference, ITP 2015, Proceedings. Zhang, X. & Urban, C. (Hrsg.). Springer Verlag, S. 310-324 15 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9236).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    19 Zitate (Scopus)

  • A verified compiler for probability density functions

    Eberl, M., Hölzl, J. & Nipkow, T., 2015, Programming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Vitek, J. (Hrsg.). Springer Verlag, S. 80-104 25 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9032).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    21 Zitate (Scopus)

  • Mining the archive of formal proofs

    Blanchette, J. C., Haslbeck, M., Matichuk, D. & Nipkow, T., 2015, Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. Kerber, M., Sorge, V., Rabe, F., Carette, J. & Kaliszyk, C. (Hrsg.). Springer Verlag, S. 3-17 15 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9150).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    32 Zitate (Scopus)

  • Verified decision procedures for MSO on words based on derivatives of regular expressions

    Traytel, D. & Nipkow, T., 9 Feb. 2015, in: Journal of Functional Programming. 25, e18.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access
    4 Zitate (Scopus)
  • 2014

    Experience report: The next 1100 Haskell programmers

    Blanchette, J. C., Hupel, L., Nipkow, T., Noschinski, L. & Traytel, D., 2014, Haskell 2014 - Proceedings of the 2014 ACM SIGPLAN Haskell Symposium. Association for Computing Machinery, S. 25-30 6 S. (Haskell 2014 - Proceedings of the 2014 ACM SIGPLAN Haskell Symposium).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • Experience Report: The Next 1100 Haskell Programmers

    Blanchette, J. C., Hupel, L., Nipkow, T., Noschinski, L. & Traytel, D., 3 Sept. 2014, in: ACM SIGPLAN Notices. 49, 12, S. 25-30 6 S.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    1 Zitat (Scopus)

  • Making security type systems less ad hoc

    Nipkow, T. & Popescu, A., 28 Dez. 2014, in: IT - Information Technology. 56, 6, S. 267-272 6 S.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access

  • Unified decision procedures for regular expression equivalence

    Nipkow, T. & Traytel, D., 2014, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, S. 450-466 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8558 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    19 Zitate (Scopus)
  • 2013

    A brief survey of verified decision procedures for equivalence of regular expressions

    Nipkow, T. & Haslbeck, M., 2013, Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings. S. 10-12 3 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8123 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • A fully verified executable LTL model checker

    Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A. & Smaus, J. G., 2013, Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings. S. 463-478 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8044 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    72 Zitate (Scopus)

  • Data refinement in Isabelle/HOL

    Haftmann, F., Krauss, A., Kunčar, O. & Nipkow, T., 2013, Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. S. 100-115 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7998 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    49 Zitate (Scopus)

  • Formalizing probabilistic noninterference

    Popescu, A., Hol̈zl, J. & Nipkow, T., 2013, Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings. S. 259-275 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8307 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    9 Zitate (Scopus)

  • Formal verification of language-based concurrent noninterference

    Popescu, A., Hölzl, J. & Nipkow, T., 2013, in: Journal of Formalized Reasoning. 6, 1, S. 1-30 30 S.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    4 Zitate (Scopus)

  • Noninterfering schedulers when possibilistic noninterference implies probabilistic noninterference

    Popescu, A., Hölzl, J. & Nipkow, T., 2013, Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings. Springer Verlag, S. 236-252 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8089 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    5 Zitate (Scopus)

  • Verified decision procedures for mso on words based on derivatives of regular expressions

    Traytel, D. & Nipkow, T., Sept. 2013, in: ACM SIGPLAN Notices. 48, 9, S. 3-12 10 S.

    Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

    Open Access
    1 Zitat (Scopus)

  • Verified decision procedures for MSO on words based on derivatives of regular expressions

    Traytel, D. & Nipkow, T., 2013, ICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming. S. 3-12 10 S. (Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    4 Zitate (Scopus)
  • 2012

    Abstract interpretation of annotated commands

    Nipkow, T., 2012, Interactive Theorem Proving - Third International Conference, ITP 2012, Proceedings. S. 116-132 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7406 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    10 Zitate (Scopus)