WING 2010: Papers with Abstracts

Abstract. The area of software analysis, testing and verification is now undergoing a revolution thanks to the use of automated and scalable support for logical methods. A well-recognized premise is that at the core of software analysis engines is invariably a component using logical formulas for describing states and transformations between system states. One can thus say that symbolic logic is the calculus of computation. The process of using this information for discovering and checking program properties (including such important properties as safety and security) amounts to automatic theorem proving. In particular, theorem provers that directly support common software constructs offer a compelling basis. Such provers are commonly called satisfiability modulo theories (SMT) solvers.
Z3 is the leading SMT solver. It is developed by the authors at Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories such as arithmetic, bit-vectors, lists, records and arrays.

This paper examines three applications of Z3 in the context of invariant generation.
The first lets Z3 infer invariants as a constraint satisfaction problem, the second application
illustrates the use of Z3 for bit-precise analysis and our third application exemplifies
using Z3 for calculations.

Abstract. We present a practical algorithm for computing least
solutions of systems of (fixpoint-)equations over the integers with,
besides other monotone operators,
addition, multiplication by positive constants, maximum, and minimum.
The algorithm is based on max-strategy iteration.
Its worst-case running-time (w.r.t. a uniform cost measure)
is independent of the sizes of occurring numbers.
We apply this
algorithm to compute the abstract semantics of
programs over integer intervals as well as over integer zones.

Abstract. We present an approach to automatically generating invariants for timed automata models. The CIPM algorithm that we propose first computes new invariants for timed automata control locations taking their originally defined invariants as well as the constrains on clock variables imposed by incoming state transitions into account. In doing so the CIPM algorithm also prunes idle transitions, which are transitions that can never be taken, from the automaton. We discsuss a prototype implementation of the CIPM algorithm as well as some initial experimental results.

Abstract. In this paper we present on-going work addressing the problem of automatically generating realistic and guaranteed correct invariants. Since invariant generation mechanisms are error-prone, after the computation of invariants by a verification tool, we formally prove that the generated invariants are indeed invariants of the considered systems using a higher-order theorem prover and automated techniques. We regard invariants for BIP models. BIP (behavior, interaction, priority) is a language for specifying asynchronous component based systems. Proving that an invariant holds often requires an induction on possible system execution traces. For this reason, apart from generating invariants that precisely capture a system’s behavior, inductiveness of invariants is an important goal. We establish a notion of robust BIP models. These can be automatically constructed from our original non-robust BIP models and over-approximate their behavior. We motivate that invariants of robust BIP models capture the behavior of systems in a more natural way than invariants of corresponding non-robust BIP models. Robust BIP models take imprecision due to values delivered by sensors into account. Invariants of robust BIP models tend to be inductive and are also invariants of the original non-robust BIP model. Therefore they may be used by our verification tools and it is easy to show their correctness in a higher-order theorem prover. The presented work is developed to verify the results of a deadlock-checking tool for embedded systems after their computations. Therewith, we gain confidence in the provided analysis results.

Abstract. We demonstrate the FLATA tool for checking reachability in counter automata using techniques which have recently been developed (such as precise acceleration of self-loops labelled by DBMs or octagons) and/or which are still under development. Apart from analysing counter automata, FLATA allows one to also reduce the given counter automata while preserving reachability of designated control locations. For demonstrating the tool, we use counter automata obtained, e.g., by translation from list manipulating programs or hardware components.

Abstract. We study automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls or code pointers. Given the specification of a procedure whose body contains calls to an unknown procedure, we try to infer the possible specifications for the unknown procedure from its calling contexts. We employ a forward shape analysis with separation logic and an abductive inference mechanism to synthesize both pre- and postconditions for the unknown procedure. The inferred specification is a partial specification of the unknown procedure. Therefore it is subject to a later verification when the code or the complete specification for the unknown procedure are available. Our inferred specifications can also be used for program understanding.

Abstract. Cocktail II is an interactive tool for deriving programs from specifications. Instead of verifying a program after it was constructed, Cocktail II aids the goal oriented derivation of a program. First, the user provides a pre- and postcondition. Then, the program to fill the gap between these condition is constructed by manually inserting statements between them. The tool computes the sub specifications of the new gaps, which can then be manually refined further. Finally, when a precondition of a gap implies its postcondition, the gap can be closed. Cocktail II also provides support for constructing the required proof. The program is complete when all gaps are closed.

Abstract. Tropical polyhedra have been recently used to represent disjunctive invariants in static analysis. To handle larger instances, the tropical analogues of classical linear programming results need to be developed. This motivation leads us to study a general tropical linear programming problem. We construct an associated parametric mean payoff game problem, and show that the optimality of a given point, or the unboundedness of the problem, can be certified by exhibiting a strategy for one of the players having certain infinitesimal properties (involving the value of the game and its derivative) that we characterize combinatorially. In other words, strategies play in tropical linear programming the role of Lagrange multipliers in classical linear programming. We use this idea to design a Newton-like algorithm to solve tropical linear programming problems, by reduction to a sequence of auxiliary mean payoff game problems.

Abstract. Hume is a Turing-complete programming language, designed to guarantee space and time bounds whilst still working on a high-level. Formal properties of Hume programs, such as invariants and transformations, have previously been verified using the temporal logic of actions (TLA). TLA properties are verified in an inductive way, which often requires lemma discovery or generalisations. Rippling was developed for guiding inductive proofs, and supports lemmas and generalisation discovery through proof critics. In this paper we show how rippling and proof critics can be used in the verification of Hume invariants represented in TLA. Our approach is based on existing work on the problem of verifying and discovering loop invariants for an imperative program. We then extend this work to Hume program transformations.

Abstract. We present CheAPS, the checker of asynchronous parameterized communicating systems. It is a set of tools for verification of parameterized families F = M_n of finite-state models against LTL specification S. Each model M_n from a family F is composed of a fixed number of control processes and n processes from a fixed set of prototypes. Given a description of a family CheAPS generates finite-state models M_n and checks if one of such models can be used as an invariant of the family. As soon as an invariant is detected it is model checked by Spin to verify it against a specification S. If Spin completes the verification successfully, then all the models of F satisfy S.

We are going to demonstrate an application of CheAPS to several examples: Chandy-Lamport snapshot algorithm, Awerbuch distributed depth-first search algorithm, Milner's scheduler, and the model of RSVP protocol, where invariants were detected successfully on that models by our tools. The project homepage is http://lvk.cs.msu.su/\~konnov/cheaps/. It is available under BSD-like license.

The full version of the abstract is uploaded.

Abstract. Loopfrog is a scalable static analyzer for ANSI-C programs, that combines the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it does not calculate the abstract fix-point of a program by iterative application of an abstract transformer. Instead, it calculates symbolic abstract transformers for program fragments (e.g., loops) using a loop summarization algorithm. Loopfrog computes abstract transformers starting from the inner-most loops, which results in linear (in the number of the looping constructs) run-time of the sum- marization procedure and which is often considerably smaller than the traditional saturation procedure of abstract interpetation. It also provides “leaping” counterexamples to aid in the diagnosis of errors.

Abstract. Currently, there are no approaches known that allow for non-termination proofs of concurrent programs which account for asynchronous communication via FIFO message queues. Those programs may be written in high-level languages such as Java or Promela. We present a first approach to prove non-termination for such programs. In addition to integers, the programs that we consider may contain queues as data structures. We present a representation of queues and the operations on them in the domain of integers, and generate invariants that help us prove non-termination of selected control flow loops using a theorem proving approach. We illustrate this approach by applying a prototype tool implementation to a number of case studies.

Abstract. We give a short overview of main functionalities and specification language of the VRS system. That environment was succesfully used for formalization and verification of ~30 software development projects implemented in Motorola. The system support both model checking and theorem proving techniques enhanced with invariants generation.

Abstract. We present a case study of the verification of parameterized mutual exclusion protocol using finite model finder Mace4. Thhe verification follows an approach based on modeling of reachability between states of the protocol as deducibility between appropriate encodings of states by first-order predicate logic formulae. The result of successful verification is a finite countermodel, a witness of non-deducibility, which represents a system invariant.

Abstract. Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them. In this paper we discuss these three concepts and analyze their relationships. The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, and may help us enhance techniques for generating invariant assertions.

Abstract. We present a technique for refining incorrect or insufficiently strong loop invariants in correctness proofs for imperative programs. We rely on previous work [16] in combining program analysis and Proof Planning, and exploit IsaPlanner’s use of meta-variables and goal-naming to generate correct loop invariants. We present a simple example in detail and show how this scales to more complex problems.

Abstract. We describe the CORE system which automatically proves fully functional specifications about pointer programs, generating functional parts of the invariants automatically where necessary.

Abstract. We describe the current state of our tool LOOPUS which computes loop bounds for C programs.

Abstract. Induction is a powerful method that can be used to prove the total correctness of program loops. Unfortunately the induction proving process in an interactive theorem prover is often very cumbersome. In particular it can be difficult to find the right induction formula. We describe a method for generalising induction formulae by analysing a symbolic proof attempt in a semi-interactive first-order theorem prover. Based on the proof attempt we introduce universally quantified variables, meta-variables and sets of constraints on these. The constraints describe the conditions for a successful proof. By the help of examples, we outline some classes of problems and their associated constraint solutions, and possible ways to automate the constraint solving.