Zafer Esen
Assistant with doctoral duties at Department of Information Technology; Division of Computer Systems
- Telephone:
- +46 18 471 23 14
- E-mail:
- zafer.esen@it.uu.se
- Visiting address:
- Hus 10, Regementsvägen 10
- Postal address:
- Box 337
751 05 UPPSALA
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.
Supervisors:
Publications
Recent publications
Transformations for Verifying Programs with Heap-Allocated Data Structures
2025
Finding Universally Quantified Heap Invariants by Horn Clause Transformations
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
Automatic Program Instrumentation for Automatic Verification
Part of CAV 2023, p. 281-304, 2023
Part of Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), p. 38-53, 2022
TRICERA: Verifying C Programs Using the Theory of Heaps
Part of Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022, p. 380-391, 2022
- DOI for TRICERA: Verifying C Programs Using the Theory of Heaps
- Download full text (pdf) of TRICERA: Verifying C Programs Using the Theory of Heaps
All publications
Comprehensive doctoral thesis
Conference papers
Finding Universally Quantified Heap Invariants by Horn Clause Transformations
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
Automatic Program Instrumentation for Automatic Verification
Part of CAV 2023, p. 281-304, 2023
Part of Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), p. 38-53, 2022
TRICERA: Verifying C Programs Using the Theory of Heaps
Part of Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022, p. 380-391, 2022
- DOI for TRICERA: Verifying C Programs Using the Theory of Heaps
- Download full text (pdf) of TRICERA: Verifying C Programs Using the Theory of Heaps
Reasoning in the Theory of Heap: Satisfiability and Interpolation
Part of LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, LOPSTR 2020, p. 173-191, 2021