今回のGRACEセミナーでは形式手法の第一人者であるウィーン工科大の Helmut Veith 教授に，分散システムに関するモデル検査技術についてご講演いただきます．
Automated Verification of Fault-Tolerant Distributed Algorithms by Model
Distributed algorithms have numerous mission-critical applications in embedded avionic and automotive systems, cloud computing, computer networks, hardware design, and the internet of things. Although distributed algorithms exhibit complex interactions with their computing environment and are difficult to understand for human engineers, computer science has developed only very limited tool support to catch logical errors in distributed algorithms at design time.
Recent work by our research group has demonstrated that the progress of the last two decades in abstract model checking, SMT solving, and partial order reduction gives leverage for parameterized model checking techniques that are able to verify, for the first time, non-trivial fault tolerant distributed algorithms. In this talk, we will survey our results and argue that model checking has acquired sufficient critical mass to build the theory and the practical tools for the formal verification of large classes of distributed algorithms.
Helmut Veith is a professor of Computer Science at Vienna University of Technology, Austria, and an Adjunct Professor at Carnegie Mellon University, Pittsburgh. Prior to his appointment in Vienna, he had professor positions at TU Darmstadt (2008-2009) and TU Munich (2003-2008). He is the speaker of the Doctoral College “Logical Methods in Computer Science”, and vice-speaker of the Austrian research network “Rigorous Systems Engineering”. Veith is a coeditor of the forthcoming Handbook of Model Checking, PC co-chair of LPAR 2008, CSL 2010, CAV 2013, and FMCAD 2015, and co-chair of the Vienna Summer of Logic 2014, the largest conference in the history of logic. He has published more than 100 papers in computer-aided verification,
software engineering, computer security, and logic in computer science. He is best known for his role in the development of Counterexample-guided Abstraction Refinement (CEGAR) which is a key ingredient in modern model checkers for software and hardware. His awards include a PhD award sub auspiciis praesidentis by the Austrian president, and an ACM Distinguished Paper Award for work on the software model checker MAGIC.