Unbounded Model Checking for ATL

In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.

A Systematic Approach to Formal Analysis of QUIC Handshake Protocol Using Symbolic Model Checking

As a newly proposed secure transport protocol, QUIC aims to improve the transport performance of HTTPS traffic and enable rapid deployment and evolution of transport mechanisms. QUIC is currently in the IETF standardization process and will potentially carry a significant portion of Internet traffic in the emerging future. An important safety goal of QUIC protocol is to provide effective data service for users. To aim this safety requirement, we propose a formal analysis method to analyze the safety of QUIC handshake protocol by using model checker SPIN and cryptographic protocol verifier ProVerif. Our analysis shows the counterexamples to safety properties, which reveal a design flaw in the current protocol specification. To this end, we also propose and verify a possible fix that is able to mitigate these flaws.

Overview of Control Algorithm Verification Methods in Power Electronics Systems

The paper presents the existing verification methods for control algorithms in power electronics systems, including the application of model checking techniques. In the industry, the most frequently used verification methods are simulations and experiments; however, they have to be performed manually and do not give a 100% confidence that the system will operate correctly in all situations. Here we show the recent advancements in verification and performance assessment of power electronics systems with the usage of formal methods. Symbolic model checking can be used to achieve a guarantee that the system satisfies user-defined requirements, while statistical model checking combines simulation and statistical methods to gain statistically valid results that predict the behavior with high confidence. Both methods can be applied automatically before physical realization of the power electronics systems, so that any errors, incorrect assumptions or unforeseen situations are detected as early as possible. An additional functionality of verification with the use of formal methods is to check the converter operation in terms of reliability in various system operating conditions. It is possible to verify the distribution and uniformity of occurrence in time of the number of transistor switching, transistor conduction times for various current levels, etc. The information obtained in this way can be used to optimize control algorithms in terms of reliability in power electronics. The article provides an overview of various verification methods with an emphasis on statistical model checking. The basic functionalities of the methods, their construction, and their properties are indicated.

Pono: A Flexible and Extensible SMT-Based Model Checker

Symbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present , an open-source SMT-based model checker. is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance, prioritizes transparency (developed as an open-source project on GitHub), flexibility ( can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers). In this paper, we describe the design of the tool with a focus on the flexible and extensible architecture, cover its current capabilities, and demonstrate that is competitive with state-of-the-art tools.