Focusing on program verification, this book offers a contemporary perspective on automata theory. It explores how the principles of automata can be applied to ensure the correctness of computer programs, making complex concepts accessible and relevant for modern applications. The approach emphasizes practical implications, bridging theoretical foundations with real-world challenges in software development.
This book constitutes the proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017, which took place in Uppsala, Sweden in April 2017, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017. The 32 papers presented in this volume were carefully reviewed and selected from 101 submissions. They were organized in topical sections named: coherence spaces and higher-order computation; algebra and coalgebra; games and automata; automata, logic and formal languages; proof theory; probability; concurrency; lambda calculus and constructive proof; and semantics and category theory.
This book constitutes the refereed proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, held in Paphos, Cyprus, in March 2010, as part of ETAPS 2010, the European Joint Conferences on Theory and Practice of Software. The 35 papers presented were carefully reviewed and selected from 134 submissions. The topics covered are probabilistic systems and optimization, decision procedures, tools, automata theory, liveness, software verification, real time and information flow, and testing.
Model checking is a prominent technique used in the hardware and software industries for automatic verification. While it is very successful in finding subtle bugs in distributed systems, it faces the state explosion problem - the number of reachable states grows exponentially in the number of concurrent components. In this book the authors introduce unfoldings, an approach to model checking which alleviates the state explosion problem by means of concurrency theory. They offer a gentle introduction to the basics of the method, and in particular they detail an unfolding-based algorithm for model checking concurrent systems against properties specified as formulas of linear temporal logic (LTL). Self-contained chapters cover transition systems and their products; unfolding products; search procedures for basic verification problems, such as reachability and livelocks; and model checking LTL. The final chapter summarizes the results of the book, and points the reader to tools and case studies. The book will be of value to researchers and graduate students engaged in automatic verification and concurrency theory.
This book constitutes the refereed proceedings of the 23rd International Conference on Application and Theory of Petri Nets, ICATPN 2002, held in Adelaide, Australia, in June 2002. The 18 regular papers and one tool presentation presented together with six invited paper were carefully reviewed and selected from 45 submissions. All current issues on research and development of Petri nets are addressed, in particular concurrent systems analysis, model validation, business process management, reactive systems, workflow processes, wireless transaction protocols.