Abstract We present $$\textsf{HornStr}$$ HornStr , the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known that invariant synthesis for RMC subsumes various important verification problems, including safety verification for parameterized systems. To achieve a simple and standardized file format, we treat the invariant synthesis problem as a problem of solving Constrained Horn Clauses (CHCs) over strings. Two strategies for synthesizing invariants in terms of regular constraints are supported: (1) L* automata learning, and (2) SAT-based automata learning. $$\textsf{HornStr}$$ HornStr implements these strategies with the help of existing SMT solvers for strings, which are interfaced through SMT-LIB. $$\textsf{HornStr}$$ HornStr provides an easy-to-use interface for string solver developers to apply their techniques to verification. At the same time, it allows verification researchers to painlessly tap into the wealth of modern string solving techniques. To assess the effectiveness of $$\textsf{HornStr}$$ HornStr , we conducted a comprehensive evaluation using benchmarks derived from applications including parameterized verification and string rewriting tasks. Our experiments highlight $$\textsf{HornStr}$$ HornStr ’s capacity to effectively handle these benchmarks, e.g., as the first solver to verify the challenging MU puzzle automatically. Finally, $$\textsf{HornStr}$$ HornStr can be used to automatically generate a new class of interesting SMT-LIB 2.6 string constraint benchmarks, which might in the future be used in the SMT-COMP strings track. In particular, our experiments on the above invariant synthesis benchmarks produce more than 30000 new constraints. We also detail the performance of various integrated string solvers, providing insights into their effectiveness on our new benchmarks.

In cyber-physical systems, the controllers are widely designed into mode-based periodic modules, which are used to control physical plants.Such a system can be modeled as a hybrid one, i.e., one of the real-time controller programs and interactive continuous plants that obey dynamical laws.In this work, to facilitate the modeling and analysis of periodic hybrid control systems in the field of aerospace and smart cities, a hierarchical hybrid modeling language (HHML) is proposed, which contains a two-hierarchy structure, i.e., mode-hierarchy and module-hierarchy.The former supports modeling a hybrid system at the abstraction level, while the latter is used to describe the behavior of the modules.The operational semantics is investigated for formal analysis, and the translation rules to hybrid automaton are explored for formal verification.A case study is conducted with the lunar lander to demonstrate the effectiveness of the approach.

As an important part of Internet of Things and 5G network technology, security protocols play a critical role in ensuring communication security.Formal analysis of security protocol has been successfully applied to find design flaws in recent years.Many formal verification tools have been used to verify the security protocols, including Murphi model checker.However, security protocols are often expressed in so-called Alice&Bob notation to describe the messages exchanged between honest principals.And security protocols defined by the A&B specifications can not be applied to the formal verification tool directly.Therefore, there is a gap between Alice&Bob specifications and the modeling languages of the formal tools.In this paper, we propose AnB2Murphi, a novel and general translator which compiles the Alice&Bob specifications of security protocols into the input language of Murphi to bridge the gap.First, we specify the Alice&Bob specifications of the security protocol.Then we take the strand space as the intermediate form between A&B specifications and Murphi formal model.Finally, we use the Murphi model checker to verify the generated model of security protocol.The case studies of security protocols like Needham-Schroeder public key protocol and 5G EAP-TLS authentication protocol demonstrate the efficiency of our translator.

Formal verification plays an important role in proving the correctness of safety-critical systems such as cache coherence protocols and security protocols. However, it usually involves rather complicated proofs which demand profound techniques in theorem proving. These techniques are too hard for those programmers with no experience in formal verification to grasp. The induction proof is a good way to reason about the properties of systems. Our work proposes a feasible approach to encode induction proof in Dafny which helps programmers to verify the systems. First, we revisit induction proof and proof dependency. Then, we decompose the complicated proof obligation into induction proof and encode the proof dependency into Dafny. Finally, we present case studies in cache coherence protocols, loop invariants and security protocols to illustrate our approach.