Software is pervading our lives. Navigation software on our favorite mobile device can prevent us from taking the car due to an unexpected oil loss and plan a convenient route using public transportation. With our software invaded laptop, we can start our work day establishing virtual meetings or performing baking operations. At the end of the lots of software applications have accompanied our social and professional activities. The increase of the role of software as a of full-day companion comes with a price: we depend more and more on it. But, can we trust software? What if a bug in the navigation system drives us to the wrong location? What if misunderstandings arise in our meeting due to a undesirable loss of QoS? What if our banking operations are being hacked? Software reliability is a must, specially when critical issues such as human integrity, privacy or security are involved. Traditionally, the computer science community has promoted the use of formal method as a means to increase the trust that we put on software. Formal specification and verification techniques have been proposed and transfered to industrial-applied technology. While it is honest to admit that not even formally developed software guarantees a complete confidence, it is widely recognized that the use of formal methods increases software reliability. Formal methods are usually seen is an auxiliary tool in software development processes, but our vision promotes the role of formal methods as a companion. Rigorous Software Development must be a formal method. Among the various formal methods we concentrate on Model Checking. Model checking is an automatic formal verification technique whose main idea is to formally specify both the system specification and its properties (typically, by means of temporal logic) and automatically verify that such properties are satisfied. The popularity of model checking has crossed the scientific borders and pervaded the industrial community and, nowadays, model checkers are being used by many companies to produce reliable software. The success of model checking has been sealed with the ACM's Turing award, received by the inventors of such technique. This series of seminars will start with a brief introduction to the fundamentals of rigorous software development and model checking. The rest of the seminars will present various model checkers (such as Spin, SMV) and model checking based development tools (such as Bandera) together with the theoretical models they are based on.