Paper "CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering" accepted at TACAS'20 and preprint available now!

Karlheinz Friedberger

Picture of Karlheinz Friedberger

Software and Computational Systems Lab
Institute for Informatics
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Room F 009, Oettingenstr. 67
+49 (89) 2180-9182


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)


Publications, Presentations, and Co (List at SoSy-Lab, List at DBLP)

  • 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