Compositional verification is a promising approach to software verification applicable to real-world programs. The idea is to analyze parts of the verified program in isolation and then compose the final result from the results of the verification of parts. The verification framework Symbiotic does not support compositional verification, in particular, its default verification backend, which is a fork of the state-of-the-art symbolic executor KLEE, does not support it. KLEE was designed to execute programs from the entry point (usually the function main()) and any attempt to start the execution from other point in the program fails on accessing non-existent memory objects. To enable analysis of program parts, such accesses must be intercepted and new objects must be lazily created to ensure that accesses to memory do not fail. The lazily allocated objects must be also properly initialized, e.g., in the case when they might contain pointers to other objects. The student will research the literature on this topic and implement some method of creating memory objects lazily into KLEE. The implementation will be thoroughly tested.