A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic

It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch–Jozsa’s algorithm and Grover's algorithm.

Symbolic and Structural Model-Checking

Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows how to solve model-checking problems using a combination of techniques that stay in complexity proportional to the size of the net structure rather than to the state-space size. We combine an SMT based over-approximation to prove that some behaviors are unfeasible, an under-approximation using memory-less sampling of runs to find witness traces or counter-examples, and a set of structural reduction rules that can simplify both the system and the property. This approach was able to win by a clear margin the model-checking contest 2020 for reachability queries as well as deadlock detection, thus demonstrating the practical effectiveness and general applicability of the system of rules presented in this paper.

Qualitative Analysis of State/Event Fault Trees Based on Interface Automata

State/Event Fault Tree (SEFT) can be used for safety modeling and assessment. However, SEFT does not provide adequate semantics for analyzing the minimal scenarios leading to system failures. In this paper, we propose a novel qualitative analysis method for SEFT based on interface automata. Firstly, we propose the concept of guarded interface automata by adding guards on interface automata transitions. Based on this model, we can describe the triggers and guards of SEFT simultaneously. Then, a weak bisimilarity operation is defined to alleviate the state space explosion problem. Based on the proposed guarded interface automata and the weak bisimilarity operation, the semantics of SEFT can be precisely determined. After that, a qualitative analysis process is presented on the basis of the formal semantics of SEFT, and the analyzing result is the minimal cut sequence set representing the causes of system failures. Finally, a fire protection system case study is illustrated step by step to demonstrate the effectiveness of our method.

One down, 699 to go: or, synthesising compositional desugarings

Programming or scripting languages used in real-world systems are seldom designed with a formal semantics in mind from the outset. Therefore, developing well-founded analysis tools for these systems requires reverse-engineering a formal semantics as a first step. This can take months or years of effort. Can we (at least partially) automate this process? Though desirable, automatically reverse-engineering semantics rules from an implementation is very challenging, as found by Krishnamurthi, Lerner and Elberty. In this paper, we highlight that scaling methods with the size of the language is very difficult due to state space explosion, so we propose to learn semantics incrementally. We give a formalisation of Krishnamurthi et al.'s desugaring learning framework in order to clarify the assumptions necessary for an incremental learning algorithm to be feasible. We show that this reformulation allows us to extend the search space and express rules that Krishnamurthi et al. described as challenging, while still retaining feasibility. We evaluate enumerative synthesis as a baseline algorithm, and demonstrate that, with our reformulation of the problem, it is possible to learn correct desugaring rules for the example source and core languages proposed by Krishnamurthi et al., in most cases identical to the intended rules. In addition, with user guidance, our system was able to synthesize rules for desugaring list comprehensions and try/catch/finally constructs.

An Incremental and Backward-Conflict Guided Method for Unfolding Petri Nets

The unfolding technique of Petri net can characterize the real concurrency and alleviate the state space explosion problem. Thus, it is greatly suitable to analyze/check some potential errors in concurrent systems. During the unfolding process of a Petri net, the calculations of configurations, cuts, and cut-off events are the key factors for the unfolding efficiency. However, most of the unfolding methods do not specify a highly efficient calculations on them. In this paper, we reveal some recursive relations and structural properties of these factors. Subsequently, we propose an improved method for computing configurations and cuts. Meanwhile, backward conflicts are used to guide the calculations of cut-off events. Moreover, a case study and a series of experiments are done to illustrate the effectiveness and application scenarios of our methods.

Replicating $$\textsc {Restart}$$ with Prolonged Retrials: An Experimental Report

Statistical model checking uses Monte Carlo simulation to analyse stochastic formal models. It avoids state space explosion, but requires rare event simulation techniques to efficiently estimate very low probabilities. One such technique is $$\textsc {Restart}$$ R E S T A R T . Villén-Altamirano recently showed—by way of a theoretical study and ad-hoc implementation—that a generalisation of $$\textsc {Restart}$$ R E S T A R T to prolonged retrials offers improved performance. In this paper, we demonstrate our independent replication of the original experimental results. We implemented $$\textsc {Restart}$$ R E S T A R T with prolonged retrials in the and tools, and apply them to the models used originally. To do so, we had to resolve ambiguities in the original work, and refine our setup multiple times. We ultimately confirm the previous results, but our experience also highlights the need for precise documentation of experiments to enable replicability in computer science.

Fuzzy particle swarm optimization algorithm (NFPSO) for reachability analysis of complex software systems

Nowadays, model checking is applied as an accuratetechnique to verify software systems. The main problem of modelchecking techniques is the state space explosion. This problemoccurs due to the exponential memory usage by the model checker.In this situation, using meta-heuristic and evolutionary algorithmsto search for a state in which a property is satisfied/violated is apromising solution. Recently, different evolutionary algorithmslike GA, PSO, etc. are applied to find deadlock state. Even thoughuseful, most of them are concentrated on finding deadlock. Thispaper proposes a fuzzy algorithm in order to analyze reachabilityproperties in systems specified through GTS with enormous statespace. To do so, we first extend the existing PSO algorithm (forchecking deadlocks) to analyze reachability properties. Then, toincrease the accuracy, we employ a Fuzzy adaptive PSO algorithmto determine which state and path should be explored in each stepto find the corresponding reachable state. These two approachesare implemented in an open-source toolset for designing andmodel checking GTS called GROOVE. Moreover, theexperimental results indicate that the hybrid fuzzy approachimproves speed and accuracy in comparison with other techniquesbased on meta-heuristic algorithms such as GA and the hybrid ofPSO-GSA in analyzing reachability properties.

An efficient statistical model checker for nondeterminism and rare events

Statistical model checking avoids the state space explosion problem in verification and naturally supports complex non-Markovian formalisms. Yet as a simulation-based approach, its runtime becomes excessive in the presence of rare events, and it cannot soundly analyse nondeterministic models. In this article, we present : a statistical model checker that combines fully automated importance splitting to estimate the probabilities of rare events with smart lightweight scheduler sampling to approximate optimal schedulers in nondeterministic models. As part of the Modest Toolset, it supports a variety of input formalisms natively and via the Jani exchange format. A modular software architecture allows its various features to be flexibly combined. We highlight its capabilities using experiments across multi-core and distributed setups on three case studies and report on an extensive performance comparison with three current statistical model checkers.