Narrow Results

Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify propertics of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be sound and complete; the properties that can be derived are exactly the valid properties. Finally some typical examples illustrate the use of the probabilistic predicates and the proof system.

We present an approach to verification of parameterized systems, which is based on program transformation technique known as supercompilation. In this approach the statements about safety properties of a system to be verified are translated into the statements about properties of the program that simulates and tests the system. Supercompilation is used then to establish the required properties of the program. In this paper we show that reachability analysis performed by supercompilation can be seen as the proof of a correctness condition by induction. We formulate suitable induction principles and proof strategies and illustrate their use by examples of verification of parameterized protocols.

Verification of program termination is an important problem in program correctness analysis. Automatically proving termination or finding nonterminating inputs as counter-examples for many programs will be a big breakthrough in theoretical computer science. A remarkable result, provided by Tiwari(2004), showed that the termination of linear loops is decidable and an eventually nonterminating input can be found for the given nonterminating loop. But some essential lemmas were missing in that proof and his algorithm could not generate a nonterminating input, which might be more widely utilized in software testing. In this paper, we discuss these details carefully and present an algorithm for producing a nonterminating input automatically. We reduce the problem of finding a nonterminating input to that of computing real root bound of a multi-exponential polynomial. This algorithm has been implemented in a Maple package based on symbolic computation. Thereby a stronger and complete decidable result in termination problem is established.

We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists.

Class temporal specification is a kind of important program specifications especially for object-oriented programs, which specifies that interface methods of a class should be called in a particular sequence. Currently, most existing approaches mine this kind of specifications based on finite state automaton. Observed that finite state automaton is a kind of deterministic models with inability to tolerate noise. In this paper, we propose to mine class temporal specifications relying on a probabilistic model extending from Markov chain. To the best of our knowledge, this is the first work of learning specifications from object-oriented programs dynamically based on probabilistic models. Different from similar works, our technique does not require annotating programs. Additionally, it learns specifications in an online mode, which can refine existing models continuously. Above all, we talk about problems regarding noise and connectivity of mined models and a strategy of computing thresholds is proposed to resolve them. To investigate our technique's feasibility and effectiveness, we implemented our technique in a prototype tool ISpecMiner and used it to conduct several experiments. Results of the experiments show that our technique can deal with noise effectively and useful specifications can be learned. Furthermore, our method of computing thresholds provides a strong assurance for mined models to be connected.

This paper shows how to verify programs manipulating recursive data structures in first-order theories with arithmetic. By extending an existed formalism, mutable data structures can be described and reasoned about more uniformly. We take Deutsch-Shorr-Waite as an example, and show that the resulting first-order theory enable us to reason about its properties in a natural way, without resorting to the loop invariants.