We are hiring new student research assistants and tutors. Apply now!
4 papers accepted at SPIN 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)

E-Mail
firstname.lastname@ifi.lmu.de
ORCID
0000-0001-7624-654X

GPG-Key

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