Automated verification of finite- or infinite state distributed systems working in network environments (e.g., in the Internet), performed via an analysis of their state spaces, is a very important and dynamic area of research, which brings promissing practical results. In the course of the previous project Automated verification of time dependent systems our group developed a model checker VerICS (available at http://pegaz.ipipan.waw.pl/~verics/), which was presented at one of the main international conferences on verification - "Tools and Algorithms for Construction and Analysis of Systems" (TACAS'03), and at the main Polish conference on real-time systems "Systemy Czasu Rzeczywistego" (SCR'03). Moreover, its results were published in more than 30 papers, which resulted in a high note given to the project by the State Committee for Scientific Research. The above-mentioned grant was directed towards theoretical problems (i.e., obtaining new verification methods, supported in a mathematical way). Conversely, the current project is orientated to practical aims, and its main goals are to prepare a programming environment enabling an easy access to VerICS, and to apply the model checker to verification of distributed software systems and cryptographic protocols.