SPIN 2014 – Proceedings

Local State Space Construction for Compositional Verification of Concurrent Systems
Hao Zheng
(University of South Florida, USA)
Local state space construction is crucial for efficient compositional verification of local and global properties of concurrent systems. This paper presents such an approach where local state transition models are built by iteratively searching the joint state space of communicating processes. The resulting local models contain less unreachable states, which would reduce false counter-examples for verifying local safety properties. Alternatively, more precise transition dependence relations can be extracted from these local models for more effective partial order reduction when the global state space is searched. The prototype of this approach has been implemented in an explicit model checker, and experimented on several concurrent examples. The initial results are encouraging.

Exploiting Synchronization in the Analysis of Shared-Memory Asynchronous Programs
Michael Emmi, Burcu Kulahcioglu Ozkan, and Serdar Tasiran
(IMDEA Software Institute, Spain; Koç University, Turkey)
As asynchronous programming becomes more mainstream, program analyses capable of automatically uncovering programming errors are increasingly in demand. Since asynchronous program analysis is computationally costly, current approaches sacrifice completeness and focus on limited sets of asynchronous task schedules that are likely to expose programming errors. These approaches are based on parameterized task schedulers, each of which admits schedules which are variations of a default deterministic schedule. By increasing the parameter value, a larger variety of schedules is explored, at a higher cost. The efficacy of these approaches depends largely on the default deterministic scheduler on which varying schedules are fashioned.
We find that the limited exploration of asynchronous program behaviors can be made more efficient by designing parameterized schedulers which better match the inherent ordering of program events, e.g., arising from waiting for an asynchronous task to complete. We follow a reduction-based "sequentialization" approach to analyzing asynchronous programs, which leverages existing (sequential) program analysis tools by encoding asynchronous program executions, according to a particular scheduler, as the executions of a sequential program. Analysis based on our new scheduler comes at no greater computational cost, and provides strictly greater behavioral coverage than analysis based on existing parameterized schedulers; we validate these claims both conceptually, with complexity and behavioral-inclusion arguments, and empirically, by discovering actual reported bugs faster with smaller parameter values.

Toward Parameterized Verification of Synchronous Distributed Applications
Sagar Chaki and James Edmondson
(Carnegie Mellon University, USA)
We present preliminary results on parameterized verification of distributed applications that assume a synchronous model of computation. Our theoretical results are negative -- the problem is undecidable even if each node has a single bit of non-determinism and the property is a 1-index safety property. Further, even if each node is completely deterministic, and the property is again a 1-index safety, parameterized verification cannot be solved via the cutoff method. Empirically, we show how to encode such applications as Array-Based Systems and verify them using existing model checkers. We demonstrate this approach on protocols for distributed mutual exclusion and collision avoidance.

Model Checking I
Mon, Jul 21, 13:30 - 15:10, Santa Clara Room (Chair: Sarfraz Khurshid)

Incremental Bounded Software Model Checking
Henning Günther and Georg Weissenbacher
(Vienna University of Technology, Austria)
Conventional Bounded Software Model Checking tools generate a symbolic representation of all feasible executions of a program up to a predetermined bound. An insufficiently large bound results in missed bugs, and a subsequent increase of the bound necessitates the complete reconstruction of the instance and a restart of the underlying solver. Conversely, exceedingly large bounds result in prohibitively large decision problems, causing the verifier to run out of resources before it can provide a result.
We present an incremental approach to Bounded Software Model Checking, which enables increasing the bound without incurring the overhead of a restart. Further, we provide an LLVM-based open-source implementation which supports a wide range of incremental SMT solvers.
We compare our implementation to other traditional non-incremental software model checkers and show the advantages of performing incremental verification by analyzing the overhead incurred on a common suite of benchmarks.

Certification for Configurable Program Analysis
Marie-Christine Jakobs and Heike Wehrheim
(University of Paderborn, Germany)
Configurable program analysis (CPA) is a generic concept for the formalization of different software analysis techniques in a single framework. With the tool CPAchecker, this framework allows for an easy configuration and subsequent automatic execution of analysis procedures ranging from data-flow analysis to model checking. The focus of the tool CPAchecker is thus on analysis. In this paper, we study configurability from the point of view of software certification. Certification aims at providing (via a prior analysis) a certificate of correctness for a program which is (a) tamper-proof and (b) more efficient to check for validity than a full analysis. Here, we will show how, given an analysis instance of a CPA, to construct a corresponding sound certification instance, thereby arriving at configurable program certification. We report on experiments with certification based on different analysis techniques, and in particular explain which characteristics of an underlying analysis allow us to design an efficient (in the above (b) sense) certification procedure.

SpinCause: A Tool for Causality Checking
Florian Leitner-Fischer and Stefan Leue
(University of Konstanz, Germany)
In this paper we present the SpinCause tool for causality checking of Promela and PRISM models. We give an overview of the capabilities of SpinCause and briefly sketch how the causality checking algorithms are integrated into the state-space exploration algorithms used for model checking. In addition we compare the runtime and memory needed for causality checking with the different state-space exploration algorithms and two newly proposed iterative causality checking approaches.

SpinRCP: The Eclipse Rich Client Platform Integrated Development Environment for the Spin Model Checker
Zmago Brezočnik, Boštjan Vlaovič, and Aleksander Vreže
(University of Maribor, Slovenia)
SpinRCP is an integrated development environment for the Spin model checker used for verifying the correctnesses of concurrent and distributed systems. Using SpinRCP, it is easy to enter, edit, examine, and check the syntax of models which represent the systems to be analyzed, to check redundancies in models, to specify the required properties of models, to graphically represent processes and never claims derived from specified properties in the form of nondeterministic final state machines, to enter or select various simulation and verification parameters, to perform verification and random, guided, or interactive simulations and to transform a Spin simulation trail into a standard Message Sequence Chart (MSC). SpinRCP is implemented in Java as an Eclipse Rich Client Platform (RCP) product.

Info

Parallel and Higher-Order Verification
Mon, Jul 21, 15:40 - 17:00, Santa Clara Room (Chair: Sagar Chaki)

Towards a GPGPU-Parallel SPIN Model Checker
Ezio Bartocci, Richard DeFrancisco, and Scott A. Smolka
(Vienna University of Technology, Austria; Stony Brook University, USA)
As General-Purpose Graphics Processing Units (GPGPUs)become more powerful, they are being used increasingly often in high-performance computing applications. State space exploration, as employed in model-checking and other verification techniques, is a large, complex problem that has successfully been ported to a variety of parallel architectures. Use of the GPU for this purpose, however, has only recently begun to be studied. We show how the 2012 multicore CPU-parallel state-space exploration algorithm of the SPIN model checker can be re-engineered to take advantage of the unique parallel-processing capabilities of the GPGPU architecture, and demonstrate how to overcome the non-trivial design obstacles presented by this task. Our preliminary results demonstrate significant performance improvements over the traditional sequential model checker for state spaces of appreciable size (>10 million unique states).

An Improvement of the Piggyback Algorithm for Parallel Model Checking
Ioannis Filippidis and Gerard J. Holzmann
(California Institute of Technology, USA; Jet Propulsion Laboratory, USA)
This paper extends the piggyback algorithm to enlarge the set of liveness properties it can verify. Its extension is motivated by an attempt to express in logic the counterexamples it can detect and relate them to bounded liveness. The original algorithm is based on parallel breadth-first search and piggybacking of accepting states that are deleted after counting a fixed number of transitions. The main improvement is obtained by renewing the counter of transitions when the same accepting states are visited in the negated property automaton. In addition, we describe piggybacking of multiple states in either sets (exact) or Bloom filters (lossy but conservative), and use of local searches that attempt to connect cycles fragmented among processing cores. Finally it is proved that accepting cycle detection is in NC in the size of the product automaton's entire state space, including unreachable states.

TravMC2: Higher-Order Model Checking for Alternating Parity Tree Automata
Robin P. Neatherway and C.-H. Luke Ong
(University of Oxford, UK)
Higher-order model checking is the problem of model checking (possibly) infinite trees generated by higher-order recursion schemes (HORS). HORS are a natural abstract model of functional programs, and HORS model checkers play a similar role to checkers of Boolean programs in the imperative setting. Most research effort so far has focused on checking safety properties specified using trivial tree automata i.e. Buechi tree automata all of whose states are final. Building on our previous work, we present a higher-order model checker, TravMC2, which supports properties specified using alternating parity tree automata (or equivalently monadic second order logic). Our experimental results offer an encouraging comparison with an existing checker, TrecS-APT.

Model Checking II
Tue, Jul 22, 10:30 - 11:50, Santa Clara Room (Chair: Stefan Leue)

Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal
Pavel Parízek and Pavel Jančík
(Charles University, Czech Republic)
Techniques and tools for verification of multi-threaded programs must cope with the huge number of possible thread interleavings. Tools based on systematic exploration of a program state space employ partial order reduction to avoid redundant thread interleavings. The key idea is to make non-deterministic thread scheduling choices only at statements that read or modify the global state shared by multiple threads. We focus on the approach to partial order reduction used in tools such as Java Pathfinder (JPF), which construct the program state space on-the-fly, and therefore can use only information available in the current program state and execution history to identify statements that may be globally-relevant. In our previous work, we developed a field access analysis that provides information about fields that may be accessed during program execution, and used it in JPF for more precise identification of globally-relevant statements. We build upon that and propose a may-happen-before analysis that computes a sound approximation of the happens-before ordering. Partial order reduction techniques can use the happens-before ordering to detect pairs of globally-relevant field access statements that cannot be interleaved arbitrarily (due to thread synchronization), and based on that avoid making unnecessary thread scheduling choices. The may-happen-before analysis combines static analysis with knowledge of information available from the dynamic program state. Results of experiments with several Java programs show that usage of the may-happen-before analysis further improves the performance of JPF.

Is There a Best Büchi Automaton for Explicit Model Checking?
František Blahoudek, Alexandre Duret-Lutz, Mojmír Křetínský, and Jan Strejček
(Masaryk University, Czech Republic; LRDE EPITA, France)
LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.

Automatic Handling of Native Methods in Java PathFinder
Nastaran Shafiei and Franck van Breugel
(NASA Ames Research Center, USA; York University, Canada)
Java PathFinder (JPF) is a model checker for Java applications. Despite its maturity, JPF cannot be used to verify any realistic Java application without a nontrivial amount of work done by its user. One of the main limiting factors towards model checking such applications is handling native calls. JPF provides ways for users to handle such calls. However, those require modeling the behaviour of the native methods in Java which is labour intensive and hinders the uptake of JPF by developers. This paper presents our tool that extends JPF to address this problem. Our work alleviates this burden for users by automatically handling native calls. Our approach is based on delegating the execution of native calls from JPF to their original execution environment. We showcase our extension by applying it to a variety of simple yet realistic Java applications that JPF, without our extension, cannot handle.

Testing and Security
Tue, Jul 22, 13:30 - 15:00, Santa Clara Room (Chair: Nastaran Shafiei)

Generic and Efficient Attacker Models in SPIN
Noomene Ben Henda
(Ericsson Research, Sweden)
In telecommunication networks, it is common that security protocol procedures rely on context information and other parameters of the global system state. Current security ver- ification tools are well suited for analyzing protocols in iso- lation and it is not clear how they can be used for protocols intended to be run in more“dynamic”settings. Think of pro- tocol procedures sharing parameters, arbitrarily interleaved or used as building blocks in more complex compound proce- dures. SPIN is a well established general purpose verification tool that has good support for modeling such systems. In contrast to specialized tools, SPIN lacks support for crypto- graphic primitives and intruder model which are necessary for checking security properties. We consider a special class of security protocols that fit well in the SPIN framework. Our modeling method is systematic, generic and efficient enough so that SPIN could find all the expected attacks on several of the classical key distribution protocols.

Quantifying Information Leaks using Reliability Analysis
Quoc-Sang Phan, Pasquale Malacaria, Corina S. Păsăreanu, and Marcelo d'Amorim
(Queen Mary University of London, UK; Carnegie Mellon University, USA; NASA Ames Research Center, USA; Federal University of Pernambuco, Brazil)
We report on our work-in-progress into the use of reliability analysis to quantify information leaks. In recent work we have proposed a software reliability analysis technique that uses symbolic execution and model counting to quantify the probability of reaching designated program states, e.g. assert violations, under uncertainty conditions in the environment. The technique has many applications beyond reliability analysis, ranging from program understanding and debugging to analysis of cyber-physical systems. In this paper we report on a novel application of the technique, namely Quantitative Information Flow analysis (QIF). The goal of QIF is to measure information leakage of a program by using information-theoretic metrics such as Shannon entropy or Renyi entropy. We exploit the model counting engine of the reliability analyzer over symbolic program paths, to compute an upper bound of the maximum leakage over all possible distributions of the confidential data.
We have implemented our approach into a prototype tool, called QILURA, and explore its effectiveness on a number of case studies.

Unit Testing for SPIN: runspin and parsepan
Theo C. Ruys
(RUwise, Netherlands)
This paper presents runspin and parsepan, two utilities to ease the verification process with the SPIN model checker. runspin allows the management of verification configurations within PROMELA models and takes care of the automatic verification.Moreover, runspin adds essential data to the verification report. parsepan is used to selectively retrieve information from verification reports. Used together the two tools can act as unit testing engine for PROMELA models.

Info

Verige: Verification with Invariant Generation Engine
Nicolas Latorre, Francesco Alberti, and Natasha Sharygina
(University of Lugano, Switzerland)
Program verification systems fail in verifying programs if appropriate loop invariants are not suggested. Generation of loop invariants in general is an art and providing them manually is a highly complex task (if possible at all). In this paper we present VERIGE, a tool that integrates a verifier with an invariant generator engine. VERIGE implements a novel generic algorithm that can alleviate the load on the invariant generator and consequently achieve a general speed-up of program verification.

Constraint-Based Analysis
Tue, Jul 22, 15:30 - 16:40, Santa Clara Room (Chair: Franjo Ivancic)

Satisfiability Modulo Abstraction for Separation Logic with Linked Lists
Aditya Thakur, Jason Breck, and Thomas Reps
(University of Wisconsin-Madison, USA; GrammaTech, USA)
Separation logic is an expressive logic for reasoning about heap structures in programs. This paper presents a semi-decision procedure for checking unsatisfiability of formulas in a fragment of separation logic that includes points-to assertions (x |-> y), acyclic-list-segment assertions (ls(x,y)), logical-and, logical-or, separating conjunction, and septraction (the DeMorgan-dual of separating implication). The fragment that we consider allows negation at leaves, and includes formulas that lie outside other separation-logic fragments considered in the literature.
The semi-decision procedure is designed using concepts from abstract interpretation. The procedure uses an abstract domain of shape graphs to represent a set of heap structures, and computes an abstraction that over-approximates the set of satisfying models of a given formula. If the over-approximation is empty, then the formula is unsatisfiable.
We have implemented the method, and evaluated it on a set of formulas taken from the literature. The implementation is able to establish the unsatisfiability of formulas that cannot be handled by previous approaches.

CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko
(TU München, Germany; Microsoft Research, UK)
Expressing program correctness often requires relating program data throughout (different branches of) an execution. Such properties can be represented using CTL+FO, a logic that allows mixing temporal and first-order quantification. Verifying that a program satisfies a CTL+FO property is a challenging problem that requires both temporal and data reasoning. Temporal quantifiers require discovery of invariants and ranking functions, while first-order quantifiers demand instantiation techniques. In this paper, we present a constraint-based method for proving CTL+FO properties automatically. Our method makes the interplay between the temporal and first-order quantification explicit in a constraint encoding that combines recursion and existential quantification. By integrating this constraint encoding with an off-the-shelf solver we obtain an automatic verifier for CTL+FO.

Towards a Test Automation Framework for Alloy
Allison Sullivan, Razieh Nokhbeh Zaeem, Sarfraz Khurshid, and Darko Marinov
(University of Texas at Austin, USA; University of Illinois at Urbana-Champaign, USA)
Writing declarative models of software designs and analyzing them to detect defects is an effective methodology for developing more dependable software systems. However, writing such models correctly can be challenging for practitioners who may not be proficient in declarative programming, and their models themselves may be buggy. We introduce the foundations of a novel test automation framework, AUnit, which we envision for testing declarative models written in Alloy -- a first-order, relational language that is supported by its SAT-based analyzer. We take inspiration from the success of the family of xUnit frameworks that are used widely in practice for test automation, albeit for imperative or object-oriented programs. The key novelty of our work is to define a basis for unit testing for Alloy, specifically, to define the concepts of test case and coverage, and coverage criteria for declarative models. We reduce the problems of declarative test execution and coverage computation to evaluation without requiring SAT solving. Our vision is to blend how developers write unit tests in commonly used programming languages with how Alloy users formulate their models in Alloy, thereby facilitating the development and testing of Alloy models for both new Alloy users as well as experts. We illustrate our ideas using a small but complex Alloy model. While we focus on Alloy, our ideas generalize to other declarative languages (such as Z, B, ASM).

SPIN 2014 – Proceedings

Frontmatter

Concurrent, Synchronous, and Asynchronous Systems
Mon, Jul 21, 10:30 - 11:50, Santa Clara Room (Chair: Willem Visser)

Model Checking I
Mon, Jul 21, 13:30 - 15:10, Santa Clara Room (Chair: Sarfraz Khurshid)

Parallel and Higher-Order Verification
Mon, Jul 21, 15:40 - 17:00, Santa Clara Room (Chair: Sagar Chaki)

Model Checking II
Tue, Jul 22, 10:30 - 11:50, Santa Clara Room (Chair: Stefan Leue)

Testing and Security
Tue, Jul 22, 13:30 - 15:00, Santa Clara Room (Chair: Nastaran Shafiei)

Constraint-Based Analysis
Tue, Jul 22, 15:30 - 16:40, Santa Clara Room (Chair: Franjo Ivancic)

SPIN 2014 – Proceedings

Frontmatter

Concurrent, Synchronous, and Asynchronous Systems Mon, Jul 21, 10:30 - 11:50, Santa Clara Room (Chair: Willem Visser)

Model Checking I Mon, Jul 21, 13:30 - 15:10, Santa Clara Room (Chair: Sarfraz Khurshid)

Parallel and Higher-Order Verification Mon, Jul 21, 15:40 - 17:00, Santa Clara Room (Chair: Sagar Chaki)

Model Checking II Tue, Jul 22, 10:30 - 11:50, Santa Clara Room (Chair: Stefan Leue)

Testing and Security Tue, Jul 22, 13:30 - 15:00, Santa Clara Room (Chair: Nastaran Shafiei)

Constraint-Based Analysis Tue, Jul 22, 15:30 - 16:40, Santa Clara Room (Chair: Franjo Ivancic)

Concurrent, Synchronous, and Asynchronous Systems
Mon, Jul 21, 10:30 - 11:50, Santa Clara Room (Chair: Willem Visser)

Model Checking I
Mon, Jul 21, 13:30 - 15:10, Santa Clara Room (Chair: Sarfraz Khurshid)

Parallel and Higher-Order Verification
Mon, Jul 21, 15:40 - 17:00, Santa Clara Room (Chair: Sagar Chaki)

Model Checking II
Tue, Jul 22, 10:30 - 11:50, Santa Clara Room (Chair: Stefan Leue)

Testing and Security
Tue, Jul 22, 13:30 - 15:00, Santa Clara Room (Chair: Nastaran Shafiei)

Constraint-Based Analysis
Tue, Jul 22, 15:30 - 16:40, Santa Clara Room (Chair: Franjo Ivancic)