The GNU Name Service Cache Daemon (NSCD) provides a cache for common name service requests. The objective of the thesis is to investigate the feasibility of formal verification of NSCD using DiVinE model checker. Student will propose and implement a set of C/C++ unit tests simulating typical interaction with NSCD, while capturing a number of important safety and liveness properties of the cache, and verifies them with DiVinE using inbuilt support for the LLVM bitcode input format. Ideally, verification should be performed with only minor modifications to the original source code. Another expected outcome of the thesis is a detailed description of all the steps needed to prepare and perform verification of a non-trivial C/C++ program using DiVinE. Investigation should conclude with a discussion on practicability of this method, including estimation of the effort required in relation to the size of the code-base, in terms of both human work and computation cost. Part of the work is also an implementation of OS and libc facilities fully emulating the environment NSCD is designated for, while still being applicable for verification with DiVinE. Most importantly, a virtual in-memory file system should be implemented and verified, exceeding the requirements of NSCD and providing all common low-level I/O functions as defined by POSIX family of standards. File system should be separable from the rest of the implementation, ready to be integrated into the set of user-space libraries shipped with DiVinE and available also for use with other projects.