Explore the vast range of titles available.

An autonomous robot case study illustrates the use of the behavior, interaction, priority (BIP) component framework as a unifying semantic model to ensure correctness of essential system design properties.

This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.

Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-horizon) linear time-invariant (LTI) models with inputs using reachability analysis. We achieve this using counterexample-guided Abstract Acceleration: this approach over-approximates the reachability tube of the LTI model over an unbounded time horizon by using abstraction, possibly finding concrete counterexamples for refinement based on the given safety specification. The technique is applied to a number of LTI models and the results show robust performance when compared to state-of-the-art tools.

Requirements-related scenarios capture typical examples of system behaviors through sequences of desired interactions between the software-to-be and its environment. Their concrete, narrative style of expression makes them very effective for eliciting software requirements and for validating behavior models. However, scenarios raise coverage problems as they only capture partial histories of interaction among-system component instances. Moreover, they often leave the actual requirements implicit. Numerous efforts have therefore been made recently to synthesize requirements or behavior models inductively from scenarios. Two problems arise from those efforts. On the one hand, the, scenarios must be complemented with additional input such as state assertions along episodes or flowcharts on such episodes. This makes such techniques difficult to use by the nonexpert end-users who provide the scenarios. On the other hand, the generated state machines may be hard to understand as their nodes generally convey no domain- specific properties. Their validation by analysts, complementary to model checking and animation by may therefore be quite difficult. This paper describes tool-supported techniques that overcome those two problems. Our tool generates a labeled transition system (LTS) for each system component from simple forms of message sequence charts (MSC) taken as examples or counterexamples of desired behavior. No additional input is required. A global LTS for the entire system is synthesized first. This LTS covers all scenario examples and excludes all counterexamples. It is inductively generated through an interactive procedure that extends known learning techniques for grammar induction. The procedure is incremental on training examples. It interactively produces additional scenarios that the end-user has to classify as examples or counterexamples of desired behavior. The LTS synthesis procedure may thus also be used independently for requirements elicitation through scenario questions generated by the tool. The synthesized system LTS is then projected on local LTS for each system component. For model validation by analysts, the tool generates state invariants that decorate the nodes of the local LTS.

A fundamental method of analyzing a system such as a program or a circuit is invariance analysis, in which one proves that an assertion holds on all reachable states. Typically, the proof is performed via induction; however, an assertion, while invariant, may not be inductive (provable via induction). Invariant generation procedures construct auxiliary inductive assertions for strengthening the assertion to be inductive. We describe a general method of generating invariants that is incremental and property-directed. Rather than generating one large auxiliary inductive assertion, our method generates many simple assertions, each of which is inductive relative to those generated before it. Incremental generation is amenable to parallelization. Our method is also property-directed in that it generates inductive assertions that are relevant for strengthening the given assertion. We describe two instances of our method: a procedure for generating clausal invariants of finite-state systems and a procedure for generating affine inequalities of numerical infinite-state systems. We provide evidence that our method scales to checking safety properties of some large finite-state systems.

This paper address the problem of generating invariants of hybrid systems. We present a new approach, for generating polynomial inequality invariants of hybrid systems through solving semi-algebraic systems and quantifier elimination. From the preliminary experiment results, we demonstrate the feasibility of our approach.

We present new computational methods that can automate the discovery and the strengthening of non-linear interrelationships among the variables of programs containing non-linear loops, that is, that give rise to multivariate polynomial and fractional relationships. Our methods have complexities lower than the mathematical foundations of the previous approaches, which used Gröbner basis computations, quantifier eliminations or cylindrical algebraic decompositions. We show that the preconditions for discrete transitions can be viewed as morphisms over a vector space of degree bounded by polynomials. These morphisms can, thus, be suitably represented by matrices. We also introduce fractional and polynomial consecution, as more general forms for approximating consecution. The new relaxed consecution conditions are also encoded as morphisms represented by matrices. By so doing, we can reduce the non-linear loop invariant generation problem to the computation of eigenspaces of specific morphisms. Moreover, as one of the main results, we provide very general sufficient conditions allowing for the existence and computation of whole loop invariant ideals. As far as it is our knowledge, it is the first invariant generation methods that can handle multivariate fractional loops.

We describe the design and implementation of an automatic invariant generator for imperative programs. While automatic invariant generation through constraint solving has been extensively studied from a theoretical viewpoint as a classical means of program verification, in practice existing tools do not scale even to moderately sized programs. This is because the constraints that need to be solved even for small programs are already too difficult for the underlying (non-linear) constraint solving engines. To overcome this obstacle, we propose to strengthen static constraint generation with information obtained from static abstract interpretation and dynamic execution of the program. The strengthening comes in the form of additional linear constraints that trigger a series of simplifications in the solver, and make solving more scalable. We demonstrate the practical applicability of the approach by an experimental evaluation on a collection of challenging benchmark programs and comparisons with related tools based on abstract interpretation and software model checking.

In this paper we discuss how to generate inductive invariants for safety verification of hybrid systems. A hybrid symbolic-numeric method is presented to compute inequality inductive invariants of the given systems. A numerical invariant of the given system can be obtained by solving a parameterized polynomial optimization problem via sum-of-squares （SOS） relaxation. And a method based on Gauss-Newton refinement and rational vector recovery is used to obtain the invariants with rational coefficients, which exactly satisfy the conditions of invariants. Several examples are given to illustrate our algorithm.

We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation. Isotopism is an important generalisation of isomorphism, and is studied by mathematicians in domains such as loop theory. This extension was not straightforward, and we had to solve two major technical problems, namely, generating and verifying isotopy invariants. Concentrating on the domain of loop theory, we have developed three novel techniques for generating isotopic invariants, by using the notion of universal identities and by using constructions based on subblocks. In addition, given the complexity of the theorems that verify that a conjunction of the invariants form an isotopy class, we have developed ways of simplifying the problem of proving these theorems. Our techniques employ an interplay of computer algebra, model generation, theorem proving, and satisfiability-solving methods. To demonstrate the power of the approach, we generate isotopic classification theorems for loops of size 6 and 7, which extend the previously known enumeration results. This work was previously beyond the capabilities of automated reasoning techniques.