Zafer Esen

Postdoctoral position at Department of Information Technology; Division of Computer Systems

E-mail:: zafer.esen@it.uu.se
Visiting address:: Hus 10, Regementsvägen 10
Postal address:: Box 524
751 20 UPPSALA

Download contact information for Zafer Esen at Department of Information Technology; Division of Computer Systems

Short presentation

Research interests (very broadly):

Analysis and verification of programs
Embedded systems and software

Tools I am currently working on:

TriCera: a model checker for C programs with heap interactions; based on Eldarica.
Eldarica: a model checker for Horn clauses, Numerical Transition Systems, and software programs accepting various inputs including SMT-LIB 2, Prolog for Horn clauses, and fragments of Scala and C for software programs.

You can visit my personal webpage for more.

Publications

Recent publications

Sound and Complete Invariant-Based Heap Encodings

Esen, Zafer; Rümmer, Philipp; Weber, Tjark

Part of Proceedings of the ACM on Programming Languages, p. 794-822, 2026
- DOI for Sound and Complete Invariant-Based Heap Encodings
- Download full text (pdf) of Sound and Complete Invariant-Based Heap Encodings
A program instrumentation framework for automatic verification

Amilon, Jesper; Esen, Zafer; Gurov, Dilian; Lidstrom, Christian et al.

Part of Formal methods in system design, 2026
- DOI for A program instrumentation framework for automatic verification
- Download full text (pdf) of A program instrumentation framework for automatic verification
Arithmetizing Shape Analysis

Wolff, Sebastian; Gupta, Ekanshdeep; Esen, Zafer; Hojjat, Hossein et al.

Part of Computer Aided Verification, p. 56-80, 2025
- DOI for Arithmetizing Shape Analysis
- Download full text (pdf) of Arithmetizing Shape Analysis
Finding Universally Quantified Heap Invariants by Horn Clause Transformations

Esen, Zafer; Rümmer, Philipp; Weber, Tjark

Part of Fundamentals of Software Engineering - 11th IFIP WG 2.2 International Conference, FSEN 2025, Västerås, Sweden, April 7-8, 2025, Proceedings, p. 42-60, 2025
- DOI for Finding Universally Quantified Heap Invariants by Horn Clause Transformations
Transformations for Verifying Programs with Heap-Allocated Data Structures

Esen, Zafer

2025
- Download full text (pdf) of Transformations for Verifying Programs with Heap-Allocated Data Structures

All publications

Articles in journal

Sound and Complete Invariant-Based Heap Encodings

Esen, Zafer; Rümmer, Philipp; Weber, Tjark

Part of Proceedings of the ACM on Programming Languages, p. 794-822, 2026
- DOI for Sound and Complete Invariant-Based Heap Encodings
- Download full text (pdf) of Sound and Complete Invariant-Based Heap Encodings
A program instrumentation framework for automatic verification

Amilon, Jesper; Esen, Zafer; Gurov, Dilian; Lidstrom, Christian et al.

Part of Formal methods in system design, 2026
- DOI for A program instrumentation framework for automatic verification
- Download full text (pdf) of A program instrumentation framework for automatic verification

Chapters in book

An Exercise in Mind Reading: Automatic Contract Inference for Frama-C

Amilon, Jesper; Esen, Zafer; Gurov, Dilian; Lidström, Christian et al.

Part of Guide to Software Verification with Frama-C, p. 553-582, Springer Nature, 2024
- DOI for An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
- Download full text (pdf) of An Exercise in Mind Reading: Automatic Contract Inference for Frama-C

Comprehensive doctoral thesis

Transformations for Verifying Programs with Heap-Allocated Data Structures

Esen, Zafer

2025
- Download full text (pdf) of Transformations for Verifying Programs with Heap-Allocated Data Structures

Conference papers