Theses

• 2025 Transformations for Verifying Programs with Heap-Allocated Data Structures
  Zafer Esen. PhD Thesis, Uppsala University.
  URL PDF
  Verifying programs that manipulate heap-allocated data structures is a long-standing challenge in software verification. This thesis summarises a series of five papers that advance the state of the art in automated verification of such programs through transformation-based approaches. The contributions include the development of a formal SMT-LIB theory of heaps to represent heap operations, the implementation of this theory in an automated verification tool for C programs, and novel invariant-based encodings that simplify reasoning about heap structures. The thesis further presents methods for automatically instrumenting programs to simplify verification tasks involving quantified properties and aggregations. All proposed techniques are fully automated and do not rely on user-provided annotations, enabling verification of heap-manipulating programs with quantified invariants that previously posed significant challenges to automated verification tools.

  @phdthesis{EsenPhD,
     author = {Esen, Zafer},
     institution = {Uppsala University, Computer Systems},
     pages = {55},
     school = {Uppsala UniversityUppsala University, Computer Systems, Division of Computer Systems},
     title = {Transformations for Verifying Programs with Heap-Allocated Data Structures},
     series = {Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology},
     ISSN = {1651-6214},
     number = {2541},
     ISBN = {978-91-513-2484-5},
     year = {2025}
  }

• 2019 Extension of the Eldarica C model checker with heap memory
  Zafer Esen. MSc Thesis, Uppsala University.
  URL PDF
  Model checking is a verification method which is used to detect bugs which would be extremely hard to detect using traditional testing, and ELDARICA is a state-of-the-art model checker which accepts a variety of formats as its input, including programs written in a fragment of the C language. This thesis aims to improve the C front-end of ELDARICA to a point where it can automatically model and verify C programs which contain pointers, heap memory interactions and structs, which are currently not supported. This work models the heap in a similar way to how it was done in JayHorn, a model checker for Java, by automatically finding quantified invariants which summarize the states of data structures that are on the heap. Support for structs is added by modeling them as algebraic data types, and limited support for stack pointers is added with some constraints on how they are declared and used. The initial experimental results are promising. The extended tool can now parse programs written in a larger fragment of the C language, with acceptable precision and performance in comparison to similar tools.

  @mastersthesis{EsenMSc,
     author = {Esen, Zafer},
     institution = {Uppsala University, Department of Information Technology},
     pages = {70},
     school = {Uppsala University, Department of Information Technology},
     title = {Extension of the ELDARICA C model checker with heap memory},
     series = {IT},
     number = {19078},
     year = {2019}
  }

Peer-Reviewed Publications

• 2025 To Appear Arithmetizing Shape Analysis
  S. Wolff, E. Gupta, Z. Esen, H. Hojjat, P. Rümmer, T. Wies. In: International Conference on Computer-Aided Verification (CAV 2025).
  URL (preprint) PDF (preprint)
  Memory safety is an essential correctness property of software systems. For programs operating on linked heap-allocated data structures, the problem of proving memory safety boils down to analyzing the possible shapes of data structures, leading to the field of shape analysis. This paper presents a novel reduction-based approach to memory safety analysis that relies on two forms of abstraction: flow abstraction, representing global properties of the heap graph through local flow equations; and view abstraction, which enable verification tools to reason symbolically about an unbounded number of heap objects. In combination, the two abstractions make it possible to reduce memory-safety proofs to proofs about heap-less imperative programs that can be discharged using off-the-shelf software verification tools without built-in support for heap reasoning. Using an empirical evaluation on a broad range of programs, the paper shows that the reduction approach can effectively verify memory safety for sequential and concurrent programs operating on different kinds of linked data structures, including singly-linked, doubly-linked, and nested lists as well as trees.

  @inproceedings{WolffEtAl2025Arithmetizing,
    title     = {Arithmetizing Shape Analysis},
    author    = {Sebastian Wolff and Ekanshdeep Gupta and Zafer Esen and Hossein Hojjat and Philipp R{\"u}mmer and Thomas Wies},
    booktitle = {CAV},
    year      = {2025},
    note      = {To appear}
  }

• 2025 Finding Universally Quantified Heap Invariants by Horn Clause Transformations
  Zafer Esen, Philipp Rümmer, Tjark Weber. In: International Conference on Fundamentals of Software Engineering (FSEN 2025).
  URL
  A common approach in software verification is to encode a program as a set of Constrained Horn Clauses (CHCs), which are then processed and solved automatically by a CHC solver. To streamline this verification approach for the case of programs operating on mutable linked data-structures, we have in earlier work proposed a theory of heaps, defined within the SMT-LIB framework, which enables us to represent programs as CHCs with minimal loss of structural information. By preserving high-level program information in the encoding, the theory of heaps enables CHC solvers to apply various internal techniques for handling program heap; among others, to encode the heap further using the theory of arrays, to apply shape analysis, or to translate to a heap-less program with the help of invariants. This paper explores the third option, developing transformation rules that rewrite a set of CHCs into an equisatisfiable set of CHCs with additional predicates representing heap invariants. The proposed method generalises the notion of space invariants, which were previously introduced for verifying Java programs, by lifting the entire transformation process to the CHC level. The paper defines the transformation rules, provides detailed correctness proofs, and discusses the strengths and limitations of the approach. We also outline possible extensions of the method.

  @InProceedings{10.1007/978-3-031-87054-5_4,
  author="Esen, Zafer
  and R{\"u}mmer, Philipp
  and Weber, Tjark",
  editor="Hojjat, Hossein
  and Caltais, Georgiana",
  title="Finding Universally Quantified Heap Invariants by Horn Clause Transformations",
  booktitle="Fundamentals of Software Engineering",
  year="2025",
  publisher="Springer Nature Switzerland",
  address="Cham",
  pages="42--60",
  isbn="978-3-031-87054-5"
  }
  

• 2024 Book Chapter An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
  J. Amilon, Z. Esen, D. Gurov, C. Lidström, P. Rümmer. Book chapter in Guide to Software Verification with Frama-C.
  URL
  Using tools for deductive verification, such as Frama-C, typically imposes substantial work overhead in the form of manually writing annotations. In this chapter, we investigate techniques for alleviating this problem by means of automatic inference of ACSL specifications. To this end, we present the Frama-C plugin Saida, which uses the assertion-based model checker TriCera as a back-end tool for inference of function contracts. TriCera transforms the program, and specifications provided as assume and assert statements, into a set of constrained Horn clauses (CHC), and relies on CHC solvers for the verification of these clauses. Our approach assumes that a C program consists of one entry-point (main) function and a number of helper functions, which are called from the main function either directly or transitively. Saida takes as input such a C program, where the main function is annotated with an ACSL function contract, and translates the contract into a harness function, comprised mainly of assume and assert statements. The harness function, together with the original program, is used as input for TriCera and, from the output of the CHC solver, TriCera infers pre- and post-conditions for all the helper functions in the C program, and translates them into ACSL function contracts. We illustrate on several examples how Saida can be used in practice, and discuss ongoing work on extending and improving the plugin.

  @Inbook{Amilon2024,
  author="Amilon, Jesper
  and Esen, Zafer
  and Gurov, Dilian
  and Lidstr{\"o}m, Christian
  and R{\"u}mmer, Philipp",
  editor="Kosmatov, Nikolai
  and Prevosto, Virgile
  and Signoles, Julien",
  title="An Exercise in Mind Reading: Automatic Contract Inference for Frama-C",
  bookTitle="Guide to Software Verification with Frama-C: Core Components, Usages, and Applications",
  year="2024",
  publisher="Springer International Publishing",
  address="Cham",
  pages="553--582",
  isbn="978-3-031-55608-1",
  doi="10.1007/978-3-031-55608-1_13",
  url="https://doi.org/10.1007/978-3-031-55608-1_13"
  }
  

• 2023 Distinguished Paper Automatic Program Instrumentation for Automatic Verification
  J. Amilon, Z. Esen, D. Gurov, C. Lidstöm, P. Rümmer. In: Int. Conf. on Computer-Aided Verification (CAV 2023).
  URL URL (extended preprint) PDF (extended preprint)
  In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.

  @InProceedings{10.1007/978-3-031-37709-9_14,
  author="Amilon, Jesper
  and Esen, Zafer
  and Gurov, Dilian
  and Lidstr{\"o}m, Christian
  and R{\"u}mmer, Philipp",
  editor="Enea, Constantin
  and Lal, Akash",
  title="Automatic Program Instrumentation for Automatic Verification",
  booktitle="Computer Aided Verification",
  year="2023",
  publisher="Springer Nature Switzerland",
  address="Cham",
  pages="281--304",
  isbn="978-3-031-37709-9"
  }
  

• 2022 TriCera: Verifying C Programs Using the Theory of Heaps
  Zafer Esen, Philipp Rümmer. In: Formal Methods in Computer-Aided Design (FMCAD 2022).
  URL PDF Slides
  TriCera is an automated, open-source verification tool for C programs based on the concept of Constrained Horn Clauses (CHCs). In order to handle programs operating on heap, TriCera applies a novel theory of heaps, which enables the tool to hand off most of the required heap reasoning directly to the underlying CHC solver. This leads to a cleaner interface between the language-specific verification front-end and the language-independent CHC back-end, and enables verification tools for different programming languages to share a common heap back-end. The paper introduces TriCera, gives an overview of the theory of heaps, and presents preliminary experimental results using SV-COMP benchmarks.

  @InProceedings{EsenTriCera,
    author={Esen, Zafer and Rümmer, Philipp},
    booktitle={2022 Formal Methods in Computer-Aided Design (FMCAD)}, 
    title={Tricera: Verifying C Programs Using the Theory of Heaps}, 
    year={2022},
    pages={380-391},
    doi={10.34727/2022/isbn.978-3-85448-053-2_45}}
  

• 2022 An SMT-LIB Theory of Heaps
  Zafer Esen, Philipp Rümmer. In: Int. Workshop on Satisfiability Modulo Theories (SMT 2022).
  (Recommended reference for the theory of heaps.)
  PDF
  Constrained Horn Clauses (CHCs) are an intermediate program representation that can be generated by several verification tools, and that can be processed and solved by a number of Horn solvers. One of the main challenges when using CHCs in verification is the encoding of heap-allocated data-structures: such data-structures are today either represented explicitly using the theory of arrays, or transformed away with the help of invariants or refinement types, defeating the purpose of CHCs as a representation that is language-independent as well as agnostic of the algorithm implemented by the Horn solver. This paper presents an SMT-LIB theory of heaps tailored to CHCs, with the goal of enabling a standard interchange format for programs with heap data-structures. We introduce the syntax of the theory of heaps, define its semantics in terms of axioms and using a reduction to SMT-LIB arrays and data-types, provide an experimental evaluation and outline possible extensions and future work.

  @inproceedings{EsenHeap22,
    author       = {Zafer Esen and
                    Philipp R{\"{u}}mmer},
    editor       = {David D{\'{e}}harbe and
                    Antti E. J. Hyv{\"{a}}rinen},
    title        = {An {SMT-LIB} Theory of Heaps},
    booktitle    = {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), Haifa, Israel, August 11-12, 2022},
    series       = {{CEUR} Workshop Proceedings},
    volume       = {3185},
    pages        = {38--53},
    publisher    = {CEUR-WS.org},
    year         = {2022},
    url          = {https://ceur-ws.org/Vol-3185/paper1180.pdf},
  }

• 2021 Reasoning in the Theory of Heap: Satisfiability and Interpolation
  Zafer Esen, Philipp Rümmer. In: Logic-Based Program Synthesis and Transformation (LOPSTR 2020). (Invited Paper)
  URL PDF (preprint)
  In recent work, we have proposed an SMT-LIB theory of heap tailored to Horn-clause verification. The theory makes it possible to lift verification approaches for heap-allocated data-structures to a language-independent level, and this way factor out the treatment of heap in verification tools. This paper gives an overview of the theory, and presents ongoing research on decision and interpolation procedures.

  @InProceedings{10.1007/978-3-030-68446-4_9,
  author="Esen, Zafer
  and R{\"u}mmer, Philipp",
  editor="Fern{\'a}ndez, Maribel",
  title="Reasoning in the Theory of Heap: Satisfiability and Interpolation",
  booktitle="Logic-Based Program Synthesis and Transformation",
  year="2021",
  publisher="Springer International Publishing",
  address="Cham",
  pages="173--191",
  isbn="978-3-030-68446-4"
  }
  

Technical Reports & Abstracts

• 2025 Under Submission Sound and Complete Invariant-Based Heap Encodings (Technical Report)
  Zafer Esen, Philipp Rümmer, Tjark Weber.
  URL PDF
  Verification of programs operating on mutable, heap-allocated data structures poses significant challenges due to potentially unbounded structures like linked lists and trees. In this paper, we present a novel relational heap encoding leveraging uninterpreted predicates and prophecy variables, reducing heap verification tasks to satisfiability checks over integers in constrained Horn clauses (CHCs). To the best of our knowledge, our approach is the first invariant-based method that achieves both soundness and completeness for heap-manipulating programs. We provide formal proofs establishing the correctness of our encodings. Through an experimental evaluation we demonstrate that our method significantly extends the capability of existing CHC-based verification tools, allowing automatic verification of programs with heap previously unreachable by state-of-the-art tools.

  @misc{esen2025soundcompleteinvariantbasedheap,
        title={Sound and Complete Invariant-Based Heap Encodings (Technical Report)}, 
        author={Zafer Esen and Philipp Rümmer and Tjark Weber},
        year={2025},
        eprint={2504.15844},
        archivePrefix={arXiv},
        primaryClass={cs.LO},
        url={https://arxiv.org/abs/2504.15844}, 
  }

• 2021 A Theory of Heap for Constrained Horn Clauses (Extended Technical Report)
  Zafer Esen, Philipp Rümmer. CoRR abs/2104.04224.
  URL PDF
  Constrained Horn Clauses (CHCs) are an intermediate program representation that can be generated by several verification tools, and that can be processed and solved by a number of Horn solvers. One of the main challenges when using CHCs in verification is the encoding of heap-allocated data-structures: such data-structures are today either represented explicitly using the theory of arrays, or transformed away with the help of invariants or refinement types, defeating the purpose of CHCs as a representation that is language-independent as well as agnostic of the algorithm implemented by the Horn solver. This paper presents an SMT-LIB theory of heap tailored to CHCs, with the goal of enabling a standard interchange format for programs with heap data-structures. We introduce the syntax of the theory of heap, define its semantics in terms of axioms and using a reduction to SMT-LIB arrays and data-types, and discuss its properties and outline possible extensions and future work.

  @misc{esen2021theoryheapconstrainedhorn,
        title={A Theory of Heap for Constrained Horn Clauses (Extended Technical Report)}, 
        author={Zafer Esen and Philipp Rümmer},
        year={2021},
        eprint={2104.04224},
        archivePrefix={arXiv},
        primaryClass={cs.LO},
        url={https://arxiv.org/abs/2104.04224}, 
  }

• 2021 A Theory of Heap for Constrained Horn Clauses
  Zafer Esen, Philipp Rümmer. Abstract at 32nd Nordic Workshop on Programming Theory (NWPT 2021).
  PDF

  @misc{EsenRuemmer2021NWPT,
    title     = {A Theory of Heap for Constrained Horn Clauses},
    author    = {Zafer Esen and Philipp R{\"u}mmer},
    booktitle = {32nd Nordic Workshop on Programming Theory},
    year      = {2021}
  }

• 2020 Towards an SMT-LIB Theory of Heap
  Zafer Esen, Philipp Rümmer. Presentation only abstract in 18th International Workshop on Satisfiability Modulo Theories (SMT 2020).
  PDF Talk (YouTube)

Invited Talks

• 2022 Eldarica and TriCera: Towards an Open Verification Framework
  Zafer Esen. At: Democratizing Software Verification Workshop (DSV 2022).
• 2021 Towards Automatic Verification of Unsafe Rust with Constrained Horn Solvers
  Z. Esen, P. Rümmer, A. Stjerna. At: Workshop on Rust for High-Integrity and Safety-Critical Systems (RustVerify 2021).