Handbook of Computer Aided Verification

Computer aided verification (CAV) refers to the practice and theory of computer-assisted formal analysis of software and hardware systems. The purpose of formal verification is to increase the dependability and safety of software and hardware systems. CAV derives concepts and findings from logic, automata theory and graph theory, and combines theoretical and experimental aspects. Research in this field encompasses model checking, automated theorem proving, synthesis and testing. It includes numerous system models such as finite-state and infinite-state systems, probabilistic systems and hybrid systems. This book elucidates the concepts and innovative models around prospective developments with respect to computer aided verification. From theories to research to practical applications, studies related to all contemporary topics of relevance to this area of computer science have been included herein. The book will serve as a valuable source of reference for graduate and postgraduate students.