Publications

Prof. Dr. Christoph Matheja

Contact

A03 202-a (» Adress and map)

Publications

Publications

  • A. -, A. L. -, and C. Matheja, "What should be observed for optimal reward in POMDPs?" CoRR, vol. abs/2405.10768.
    doi: 10.48550/ARXIV.2405.10768
  • M. Kuhn, J. Grüger, C. Matheja, and A. Rivkin, "Data Petri Nets meet Probabilistic Programming (Extended version)" CoRR, vol. abs/2406.11883.
    doi: 10.48550/ARXIV.2406.11883
  • [inproceedings] bibtex | Go to document
    M. Kuhn, J. Grüger, C. Matheja, and A. Rivkin, "Data Petri Nets Meet Probabilistic Programming" in Proc. Business Process Management - 22nd International Conference, BPM 2024, Krakow, Poland, September 1-6, 2024, Proceedings, 2024.
    doi: 10.1007/978-3-031-70396-6_2
  • [inproceedings] bibtex | Go to document
    A. -, A. L. -, and C. Matheja, "What Should Be Observed for Optimal Reward in POMDPs?" in Proc. Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III, 2024.
    doi: 10.1007/978-3-031-65633-0_17
  • P. Schröer, K. Batz, B. L. Kaminski, J. -, and C. Matheja, "A Deductive Verification Infrastructure for Probabilistic Programs" CoRR, vol. abs/2309.07781.
    doi: 10.48550/ARXIV.2309.07781
  • K. Batz, B. L. Kaminski, J. -, C. Matheja, and L. Verscht, "A Calculus for Amortized Expected Runtimes" Proc. ACM Program. Lang. vol. 7, iss. POPL.
    doi: 10.1145/3571260
  • P. Schröer, K. Batz, B. L. Kaminski, J. -, and C. Matheja, "A Deductive Verification Infrastructure for Probabilistic Programs" Proc. ACM Program. Lang. vol. 7, iss. OOPSLA2.
    doi: 10.1145/3622870
  • C. Matheja, J. Pagel, and F. Zuleger, "A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions" ACM Trans. Comput. Log. vol. 24, iss. 1.
    doi: 10.1145/3534927
  • P. Schröer, K. Batz, B. L. Kaminski, J. -, and C. Matheja. () A Deductive Verification Infrastructure for Probabilistic Programs - Artifact Evaluation (Version 1). [Online]. Available: https://doi.org/10.5281/zenodo.8146987
    doi: 10.5281/ZENODO.8146987
  • [inproceedings] bibtex | Go to document
    K. Batz, M. Chen, S. Junges, B. L. Kaminski, J. -, and C. Matheja, "Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants" in Proc. Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, 2023.
    doi: 10.1007/978-3-031-30820-8_25
  • K. Batz, I. Fesefeldt, M. Jansen, J. -, F. Keßler, C. Matheja, and T. Noll, "Foundations for Entailment Checking in Quantitative Separation Logic (extended version)" CoRR, vol. abs/2201.11464.
  • K. Batz, M. Chen, S. Junges, B. L. Kaminski, J. -, and C. Matheja, "Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants" CoRR, vol. abs/2205.06152.
    doi: 10.48550/ARXIV.2205.06152
  • K. Batz, B. L. Kaminski, J. -, C. Matheja, and L. Verscht, "A Calculus for Amortized Expected Runtimes" CoRR, vol. abs/2211.12923.
    doi: 10.48550/ARXIV.2211.12923
  • [inproceedings] bibtex | Go to document
    K. Batz, I. Fesefeldt, M. Jansen, J. -, F. Keßler, C. Matheja, and T. Noll, "Foundations for Entailment Checking in Quantitative Separation Logic" in Proc. Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, 2022.
    doi: 10.1007/978-3-030-99336-8_3
  • [inproceedings] bibtex | Go to document
    V. Astrauskas, A. B\'. i, J. Fiala, Z. Grannan, C. Matheja, P. Müller, F. Poli, and A. J. Summers, "The Prusti Project: Formal Verification for Rust" in Proc. NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings, 2022.
    doi: 10.1007/978-3-031-06773-0_5
  • K. Batz, M. Chen, B. L. Kaminski, J. -, C. Matheja, and P. Schröer, "Latticed k-Induction with an Application to Probabilistic Programs" CoRR, vol. abs/2105.14100.
  • A. B\'. i, C. Matheja, and P. Müller, "Flexible Refinement Proofs in Separation Logic" CoRR, vol. abs/2110.13559.
  • A. Aguirre, G. Barthe, J. Hsu, B. L. Kaminski, J. -, and C. Matheja, "A pre-expectation calculus for probabilistic sensitivity" Proc. ACM Program. Lang. vol. 5, iss. POPL.
    doi: 10.1145/3434333
  • K. Batz, B. L. Kaminski, J. -, and C. Matheja, "Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning" Proc. ACM Program. Lang. vol. 5, iss. POPL.
    doi: 10.1145/3434320
  • F. Wolff, A. B\'. i, C. Matheja, P. Müller, and A. J. Summers, "Modular specification and verification of closures in Rust" Proc. ACM Program. Lang. vol. 5, iss. OOPSLA.
    doi: 10.1145/3485522
  • [inproceedings] bibtex | Go to document
    K. Batz, M. Chen, B. L. Kaminski, J. -, C. Matheja, and P. Schröer, "Latticed k-Induction with an Application to Probabilistic Programs" in Proc. Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, 2021.
    doi: 10.1007/978-3-030-81688-9_25
  • [inproceedings] bibtex | Go to document
    I. Fesefeldt, C. Matheja, T. Noll, and J. Schulte, "Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars" in Proc. Graph Transformation - 14th International Conference, ICGT 2021, Held as Part of STAF 2021, Virtual Event, June 24-25, 2021, Proceedings, 2021.
    doi: 10.1007/978-3-030-78946-6_15
  • [phdthesis] bibtex | Go to document
    C. Matheja, "Automated reasoning and randomization in separation logic" PhD Thesis , 2020.
  • J. Pagel, C. Matheja, and F. Zuleger, "Complete Entailment Checking for Separation Logic with Inductive Definitions" CoRR, vol. abs/2002.01202.
  • K. Batz, S. Junges, B. L. Kaminski, J. -, C. Matheja, and P. Schröer, "PrIC3: Property Directed Reachability for MDPs" CoRR, vol. abs/2004.14835.
  • K. Batz, B. L. Kaminski, J. -, and C. Matheja, "Relatively Complete Verification of Probabilistic Programs" CoRR, vol. abs/2010.14548.
  • V. Astrauskas, C. Matheja, F. Poli, P. Müller, and A. J. Summers, "How do programmers use unsafe rust?" Proc. ACM Program. Lang. vol. 4, iss. OOPSLA.
    doi: 10.1145/3428204
  • [inproceedings] bibtex | Go to document
    K. Batz, S. Junges, B. L. Kaminski, J. -, C. Matheja, and P. Schröer, "PrIC3: Property Directed Reachability for MDPs" in Proc. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, 2020.
    doi: 10.1007/978-3-030-53291-8_27
  • A. Aguirre, G. Barthe, J. Hsu, B. L. Kaminski, J. -, and C. Matheja, "Kantorovich Continuity of Probabilistic Programs" CoRR, vol. abs/1901.06540.
  • B. L. Kaminski, J. -, and C. Matheja, "On the hardness of analyzing probabilistic programs" Acta Informatica, vol. 56, iss. 3.
    doi: 10.1007/S00236-018-0321-1
  • K. Batz, B. L. Kaminski, J. -, C. Matheja, and T. Noll, "Quantitative separation logic: a logic for reasoning about probabilistic pointer programs" Proc. ACM Program. Lang. vol. 3, iss. POPL.
    doi: 10.1145/3290347
  • [inproceedings] bibtex | Go to document
    J. Katelaan, C. Matheja, and F. Zuleger, "Effective Entailment Checking for Separation Logic with Inductive Definitions" in Proc. Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, 2019.
    doi: 10.1007/978-3-030-17465-1_18
  • [inproceedings] bibtex | Go to document
    M. Sighireanu, J. A. N. Pérez, A. Rybalchenko, N. Gorogiannis, R. Iosif, A. Reynolds, C. Serban, J. Katelaan, C. Matheja, T. Noll, F. Zuleger, W. -, Q. L. Le, Q. -, T. -, T. -, S. -, M. Cyprian, A. Rogalewicz, T. Vojnar, C. Enea, O. Lengál, C. Gao, and Z. Wu, "SL-COMP: Competition of Solvers for Separation Logic" in Proc. 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, 2019.
    doi: 10.1007/978-3-030-17502-3_8
  • K. Batz, B. L. Kaminski, J. -, and C. Matheja, "How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times" CoRR, vol. abs/1802.10433.
  • K. Batz, B. L. Kaminski, J. -, C. Matheja, and T. Noll, "Quantitative Separation Logic" CoRR, vol. abs/1802.10467.
  • B. L. Kaminski, J. -, C. Matheja, and F. Olmedo, "Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms" J. ACM, vol. 65, iss. 5.
    doi: 10.1145/3208102
  • [inproceedings] bibtex | Go to document
    H. Arndt, C. Jansen, J. -, C. Matheja, and T. Noll, "Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs" in Proc. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, 2018.
    doi: 10.1007/978-3-319-96142-2_1
  • [inproceedings] bibtex | Go to document
    K. Batz, B. L. Kaminski, J. -, and C. Matheja, "How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times" in Proc. 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, Thessaloniki, Greece, April 14-20, 2018, Proceedings, 2018.
    doi: 10.1007/978-3-319-89884-1_7
  • [inproceedings] bibtex | Go to document
    J. Katelaan, C. Matheja, T. Noll, and F. Zuleger, "Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic" in Proc. LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018, 2018.
    doi: 10.29007/QWD8
  • [inproceedings] bibtex | Go to document
    H. Arndt, C. Jansen, C. Matheja, and T. Noll, "Graph-Based Shape Analysis Beyond Context-Freeness" in Proc. Software Engineering and Formal Methods - 16th International Conference, SEFM 2018, Held as Part of STAF 2018, Toulouse, France, June 27-29, 2018, Proceedings, 2018.
    doi: 10.1007/978-3-319-92970-5_17
  • [inproceedings] bibtex | Go to document
    M. van Keulen, B. L. Kaminski, C. Matheja, and J. -, "Rule-Based Conditioning of Probabilistic Data" in Proc. Scalable Uncertainty Management - 12th International Conference, SUM 2018, Milan, Italy, October 3-5, 2018, Proceedings, 2018.
    doi: 10.1007/978-3-030-00461-3_20
  • H. Arndt, C. Jansen, C. Matheja, and T. Noll, "Heap Abstraction Beyond Context-Freeness" CoRR, vol. abs/1705.03754.
  • [inproceedings] bibtex | Go to document
    C. Jansen, J. Katelaan, C. Matheja, T. Noll, and F. Zuleger, "Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic" in Proc. Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, 2017.
    doi: 10.1007/978-3-662-54434-1_23
  • C. Jansen, J. Katelaan, C. Matheja, T. Noll, and F. Zuleger, "Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic" CoRR, vol. abs/1610.07041.
  • B. L. Kaminski, J. -, and C. Matheja, "Inferring Covariances for Probabilistic Programs" CoRR, vol. abs/1606.08280.
  • B. L. Kaminski, J. -, C. Matheja, and F. Olmedo, "Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs" CoRR, vol. abs/1601.01001.
  • F. Olmedo, B. L. Kaminski, J. -, and C. Matheja, "Reasoning about Recursive Probabilistic Programs" CoRR, vol. abs/1603.02922.
  • [inproceedings] bibtex | Go to document
    F. Olmedo, B. L. Kaminski, J. -, and C. Matheja, "Reasoning about Recursive Probabilistic Programs" in Proc. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, 2016.
    doi: 10.1145/2933575.2935317
  • [inproceedings] bibtex | Go to document
    B. L. Kaminski, J. -, C. Matheja, and F. Olmedo, "Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs" in Proc. Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, 2016.
    doi: 10.1007/978-3-662-49498-1_15
  • [inproceedings] bibtex | Go to document
    B. L. Kaminski, J. -, and C. Matheja, "Inferring Covariances for Probabilistic Programs" in Proc. Quantitative Evaluation of Systems - 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings, 2016.
    doi: 10.1007/978-3-319-43425-4_14
  • [inproceedings] bibtex | Go to document
    C. Matheja, C. Jansen, and T. Noll, "Tree-Like Grammars and Separation Logic" in Proc. Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, 2015.
    doi: 10.1007/978-3-319-26529-2_6
(Changed: 10 Sep 2024)  | 
Zum Seitananfang scrollen Scroll to the top of the page