WING on Wednesday, July 21st

09:00‑10:00 Invited Talk
Location: AT 2.11
09:00 Helmut Seidl
Abstract Interpretation Meets Mathematical Optimization
10:30‑12:28 Regular Papers and Tool Demos
Location: AT 2.11
10:30 Stephane Gaubert, Ricardo Katz and Sergei Sergeev
Tropical linear programming and parametric mean payoff games

We study a general tropical linear programming problem: we look for a point in a max-plus polyhedron minimizing the ratio of two max-plus affine forms. 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 of one player having certain infinitesimal properties (involving the value of the game and its derivative) that we characterize combinatorially, In other words, strategies seem to play in tropical linear programming the role of Lagrange multipliers in classical linear programming. We use this idea to design a Netwon-like algorithm to solve a tropical linear programming problem, by reduction to a sequence of auxiliary mean-payoff game problems.

11:00 Michael Franssen
Cocktail II

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.

11:22 Igor Konnov
CheAPS: a Checker of Asynchronous Parameterized Systems

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.

11:44 Ewen Maclean, Andrew Ireland and Gudmund Grov
Synthesising Functional Invariants in Separation Logic

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

12:06 Florian Zuleger and Moritz Sinn
LOOPUS - A Tool for Computing Loop Bounds for C Programs

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

14:00‑15:00 Invited Talk
Location: AT 2.11
14:00 Sumit Gulwani
Methods for Loop Invariant Generation
15:30‑17:28 Regular Papers and Tool Demos
Chair: Andrei Voronkov
Location: AT 2.11
15:30 Matthias Kuntz, Stefan Leue and Christoph Scheben
Extending Non-Termination Proof Techniques to Communicating Asynchronous Concurrent Programs

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.

16:00 Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich and Christoph M. Wintersteiger
Loopfrog — loop summarization for static analysis

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.

16:22 Vlad Volkov, Alexander Letichevsky, Alexander Kolchin, Oleksandr Letychevskyy jr., Stepan Potiyenko and Thomas Weigert
Formal Requirements Capturing using VRS system

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.

16:44 Alexei Lisitsa
Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol

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.

17:06 Radu Iosif, Marius Bozga, Filip Konecny and Tomas Vojnar
Tool Demonstration of the FLATA Counter Automata Toolset

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.