We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
Distinguished Paper Award and Best Artifact Award at FSE 2024!

Dr. Karlheinz Friedberger

Picture of Dr. Karlheinz Friedberger

Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)



Please send me encrypted mails!
My GPG key: 0xACCD6DC1
Fingerprint: 8C88 203A 21B7 5B34 78E3 DAFB 4D6D 84D3 ACCD 6DC1

Teaching & Organization

LMU Munich:

University of Passau:

  • WS 2016/17: Programmierung 2 (Übung)
  • SS 2016: Software Engineering (Übung), Sommercamp Informatik
  • WS 2015/16: Programmierung 2 (Übung), Entwurfsautomatisierung (Übung)

Project Participation

Publications, Presentations, and Co (Full list on website, List at DBLP)

  • Dissertation / PhD Thesis 2021: Effcient Software Model Checking with Block-Abstraction Memoization doi, pdf, slides
  • ATVA 2021: PJBDD: A BDD Library for Java and Multi-Threading, doi, pdf
  • CAV 2021: JavaSMT 3: Interacting with SMT Solvers in Java, doi, pdf, video
  • ISoLA 2020: Violation Witnesses and Result Validation for Multi-Threaded Programs, pdf, supplementary website
  • ESEC/FSE 2020: Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization, doi, pdf, video, supplementary artifact
  • ISoLA 2018: In-Place vs. Copy-on-Write CEGAR Refinement for Block Summarization with Caching, pdf, slides, supplementary website
  • CPA 2018: Domain-Independent Multi-threaded Software Model Checking, slides
  • ASE 2018: Domain-Independent Multi-threaded Software Model Checking, pdf, supplementary website
  • AVM 2017: Block-Abstraction Memoization with CEGAR (In-Place vs. Copy-On-Write Refinement), poster
  • CPA 2017: Block Abstraction Memoization with Copy-On-Write Refinement, slides
  • TACAS 2017: CPAchecker for Reachability, Memory Safety, Overflows, Concurrency, and Termination (Competition Contribution), poster
  • TACAS 2017: CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution), doi
  • MEMICS 2016: A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker, doi, pdf
  • CPA 2016: A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker, slides
  • RERS 2016: Gold medal in Reachability Plain and silver medal in Reachability Arithmetic, results
  • VSTTE 2016: JavaSMT: A Unified Interface for SMT Solvers in Java, doi, project
  • TACAS 2016: CPA-BAM: Block-Abstraction Memoization in CPAchecker (Competition Contribution), doi, pdf, slides
  • Master's Thesis 2015: Block-Abstraction Memoization as an Approach to Verify Recursive Procedures, pdf
  • HVC 2013: Domain Types: Abstract-Domain Selection Based on Variable Usage, doi, pdf
  • Bachelor's Thesis 2012: Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken, pdf