Семинар ПОИС: "Finite countermodel finding for the infinite-state and parameterized verification"

Traditional model checking has been very successful in the verification of finite state systems. In many cases, though the finite state abstraction is not enough, as we might need to verify the algorithm or protocol for essentially unbounded computation/execution, e. g.  to ensure that a protocol is correct for **any number** of participants or for **any size** of a data structure. In such cases, we are facing infinite state, or parameterized systems, the verification of which in general is an undecidable problem.  

 In this talk, we introduce a conceptually simple but powerful and efficient method for automated safety verification of infinite-state and parameterized system. The method utilises modelling of reachability between the states of a system as derivability in the classical first-order (FO) logic. With such modelling to establish the safety of a system, that is non-reachability of unsafe states, it is sufficient to show that a particular first-order formula is not provable. In this FCM method, the latter task is delegated to the available automated finite model finding procedures. 

In the talk, we present theoretical foundations, discuss the relative completeness of the method and illustrate the method by numerous applications for infinite-state and parameterized verification tasks.