WING 2010: Papers with AbstractsPapers 

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 wellrecognized 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, bitvectors, 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 bitprecise 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 maxstrategy iteration. Its worstcase runningtime (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 ongoing work addressing the problem of automatically generating realistic and guaranteed correct invariants. Since invariant generation mechanisms are errorprone, 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 higherorder 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 nonrobust BIP models and overapproximate their behavior. We motivate that invariants of robust BIP models capture the behavior of systems in a more natural way than invariants of corresponding nonrobust 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 nonrobust BIP model. Therefore they may be used by our verification tools and it is easy to show their correctness in a higherorder theorem prover. The presented work is developed to verify the results of a deadlockchecking 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 selfloops 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 heapmanipulating 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 Newtonlike algorithm to solve tropical linear programming problems, by reduction to a sequence of auxiliary mean payoff game problems.  Abstract. Hume is a Turingcomplete programming language, designed to guarantee space and time bounds whilst still working on a highlevel. 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 finitestate 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 finitestate 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: ChandyLamport snapshot algorithm, Awerbuch distributed depthfirst 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 BSDlike license.
The full version of the abstract is uploaded.  Abstract. Loopfrog is a scalable static analyzer for ANSIC 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 ﬁxpoint 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 innermost loops, which results in linear (in the number of the looping constructs) runtime 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 nontermination proofs of concurrent programs which account for asynchronous communication via FIFO message queues. Those programs may be written in highlevel languages such as Java or Promela. We present a ﬁrst approach to prove nontermination 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 nontermination of selected control ﬂow 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 firstorder predicate logic formulae. The result of successful verification is a finite countermodel, a witness of nondeducibility, 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 metavariables and goalnaming 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 semiinteractive firstorder theorem prover. Based on the proof attempt we introduce universally quantified variables, metavariables 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. 

