Model checking: Novel techniques and applications

Model checking is a formal approach for software verification. It can prove mathematically the absence of certain types of malicious behaviors, such as deadlocks. Because model checking exhaustively explores all possible states and transitions of given software system, its sluggish performance has impeded broad application in software development.; Recent progress on leveraging the performance sheds light on its massive adoption in daily practices. One key contribution of this dissertation is an innovative model checking technique, proof slicing, that simultaneously reduces running time and storage requirement. Theoretical results have shown that proof slicing subsumes several existing abstraction-based, counterexample-driven model checking approaches, such as Lazy Abstraction, Craig Interpolation, and Localization. Experimental data have shown the superior performance in both running time and storage requirement of Blade, the model checker that implements proof slicing technique, over existing model checkers, such as BLAST from University of California at Berkeley.; Web services and Services-Oriented Architecture (SOA) is a new paradigm for software development. SOA provide uniform data marshaling protocols (via Simple Object Access Protocol: SOAP and eXtensible Markup Language: XML), consistent information exchange infrastructure (via Web Service Definition Language: WSDL and HyperText Transfer Protocol: HTTP), and service query facility (via Universal Description, Discovery, and Integration: UDDI). New applications can be composed rapidly with SOA. Moreover, existing applications can be easily reconfigured or recomposed to meet new functional or non-functional requirements. The rapid development permitted by SOA imposes challenges on dynamic verification and validation on the newly developed applications. This dissertation reports an automated verification and validation framework powered by proof slicing and other techniques and its applications to dynamic verification and validation. This dissertation also reports the application of model checking techniques to the verification of service collaboration.