Search

We present “Verified JavaBIP”, a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and synchronization annotations. While JavaBIP guarantees execution progresses according to the indicated state machines, it does not guarantee properties of the data exchanged between components. It also does not provide verification support to check whether the behaviour of the resulting concurrent program is as (safe as) expected. This paper addresses this by extending the JavaBIP engine with run-time verification support, and by extending the program verifier VerCors to verify JavaBIP models deductively. These two techniques complement each other: feedback from run-time verification allows quicker prototyping of contracts, and deductive verification can reduce the overhead of run-time verification. We demonstrate our approach on the “Solidity Casino” case study, known from the VerifyThis Collaborative Long Term Challenge.

This report documents the program and the outcomes of Dagstuhl Seminar 22451 "Principles of Contract Languages". At the seminar, participants discussed the fundamental aspects of software contracts. Topics included the format and expressiveness of contracts, their use cases in software development and analysis, and contract composition and decomposition., DagRep, Volume 12, Issue 11, pages 1-27

This paper presents a case study where a concurrent module of a tunnel control system written in Java is verified for memory safety and data race freedom using VerCors, a software verification tool. This case study was carried out in close collaboration with our industrial partner Technolution, which is in charge of developing the tunnel control software. First, we describe the process of preparing the code for verification, and how we make use of the different capabilities of VerCors to successfully verify the module. The concurrent module has gone through a rigorous process of design, code reviewing and unit and integration testing. Despite this careful approach, VerCors found two memory related bugs. We describe these bugs, and show how VerCors could have found them during the development process. Second, we wanted to communicate back our results and verification process to the engineers of Technolution. We discuss how we prepared our presentation, and the explanation we settled on. Third, we present interesting feedback points from this presentation. We use this feedback to determine future work directions with the goal to improve our tool support, and to bridge the gap between formal methods and industry.

We motivate and summarise the track SpecifyThis – Bridging gaps between program specification paradigms, taking place at the International Symposium on Leveraging Applications of Formal Methods, ISoLA 2022.

Dedicated many-core processors such as GPGPUs, enable programmers to design and implement parallel algorithms to optimize performance. The stream compaction and summed-area table algorithms are two examples where parallel versions have been proposed in the literature with substantial speed ups compared to sequential counterparts. Since these two algorithms are widely used, their correctness is of the utmost importance, i.e., the algorithms must be functionally correct and their implementations must be memory safe. These algorithms use the parallel prefix sum algorithm internally. In our previous work, we verified two parallel prefix sum algorithms. In this paper, we show how we can reuse a verified sub-function (i.e., prefix sum) to prove more complicated algorithms (i.e., stream compaction and summed area table) in a modular way with less effort. Moreover, we demonstrate that it is feasible in practice to verify larger case studies by building the verification of the complicated algorithm on top of the basic one. To show the correctness of the algorithms, we use deductive program verification based on permission-based separation logic, which is supported by the program verifier VerCors. To the best of our knowledge, we are the first to verify functional correctness of the parallel stream compaction and summed-area table algorithms for an arbitrary array size, using tool support.

Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness .

Although software verification is evolving fast in both theoretical and practical aspects, it still remains absent from the actual industrial production cycle. Case studies can help to encourage these integrations. We report on our experiences applying software verification in several projects with industry. In particular, we report on two projects on the verification of tunnel control software at Technolution, where we go from a high-level design to concrete code. These case studies show the power of combining model checking (using mCRL2) and deductive verification (using VerCors) as complementary approaches. We also report on a project with Thales, where we looked at antenna bearing control software, and specified this based on their requirements documents. For all cases, we report on lessons learned and on directions for future work to improve both our tool and the industrial methodology for ensuring software correctness. Notably, our second case study involves the modelling and verification of critical software by a team of engineers from Technolution. This case study is an ongoing project; we describe our experience on the team’s learning curve for this experiment and present the preliminary conclusions on the case study.

Formal analysis techniques for software systems are becoming more and more powerful, and have been used on non-trivial examples. We argue that the next step forward is to combine these different techniques in a single framework, which makes it possible to (i) analyse different parts of the system with different techniques, (ii) apply different techniques on a single component, and (iii) seamlessly combine the results of the various analysis. We describe our vision of how this integration can be achieved for the analysis techniques of testing and deductive verification. We end with an overview of research challenges that need to be addressed to achieve this vision.

With the progress in deductive program verification research, new tools and techniques have become available to support design-by-contract reasoning about non-trivial programs written in widely-used programming languages. However, deductive program verification remains an activity for experts, with ample experience in programming, specification and verification. We would like to change this situation, by developing program verification techniques that are available to a larger audience. In this paper, we present how we developed program verification support for Snap!. Snap! is a visual programming language, aiming in particular at high school students. We added specification language constructs in a similar visual style, designed to make the intended semantics clear from the look and feel of the specification constructs. We provide support both for static and dynamic verification of Snap! programs. Special attention is given to the error messaging, to also make this as intuitive as possible. Finally, we outline how program verification in Snap! could be introduced to high school students in a classroom situation.

We study the problem of finding optimal strategies in Markov decision processes with lexicographic ω -regular objectives, which are ordered collections of ordinary ω -regular objectives. The goal is to compute strategies that maximise the probability of satisfaction of the first ω -regular objective; subject to that, the strategy should also maximise the probability of satisfaction of the second ω -regular objective; then the third and so forth. For instance, one may want to guarantee critical requirements first, functional ones second and only then focus on the non-functional ones. We show how to harness the classic off-the-shelf model-free reinforcement learning techniques to solve this problem and evaluate their performance on four case studies.

This paper covers the Rigorous Examination of Reactive Systems (RERS) Challenge 2019. For the first time in the history of RERS, the challenge features industrial tracks where benchmark programs that participants need to analyze are synthesized from real-world models. These new tracks comprise LTL, CTL, and Reachability properties. In addition, we have further improved our benchmark generation infrastructure for parallel programs towards a full automation. RERS 2019 is part of TOOLympics, an event that hosts several popular challenges and competitions. In this paper, we highlight the newly added industrial tracks and our changes in response to the discussions at and results of the last RERS Challenge in Cyprus.

Quantitative formal models capture probabilistic behaviour, real-time aspects, or general continuous dynamics. A number of tools support their automatic analysis with respect to dependability or performance properties. QComp 2019 is the first, friendly competition among such tools. It focuses on stochastic formalisms from Markov chains to probabilistic timed automata specified in the Jani model exchange format, and on probabilistic reachability, expected-reward, and steady-state properties. QComp draws its benchmarks from the new Quantitative Verification Benchmark Set. Participating tools, which include probabilistic model checkers and planners as well as simulation-based tools, are evaluated in terms of performance, versatility, and usability. In this paper, we report on the challenges in setting up a quantitative verification competition, present the results of QComp 2019, summarise the lessons learned, and provide an outlook on the features of the next edition of QComp.

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non-punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non-punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non-punctuality called non-adjacency for TPTL[U,S], and focus on its 1-variable fragment, 1-TPTL[U,S]. While non-adjacent 1-TPTL[U,S] appears to be a very small fragment, it is strictly more expressive than MITL. As our main result, we show that the satisfiability checking problem for non-adjacent 1-TPTL[U,S] is decidable with EXPSPACE complete complexity.

How to improve the recruitment, onboarding and promotion of women in computer science? The IPN working group on Equity, Diversity and Inclusion recently published a report with five practical recommendations.

arXiv

VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties---something that lies beyond the capabilities of fully automatic verification, and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned two days of work. The report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

Techniques are required that support developers to produce GPU software that is both functionally correct and high-performing. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years.

String sanitizers are widely used functions for preventing injection attacks such as SQL injections and cross-site scripting (XSS). It is therefore crucial that the implementations of such string sanitizers are correct. We present a novel approach to reason about a sanitizer's correctness by automatically generating a model of the implementation and comparing it to a model of the expected behaviour. To automatically derive a model of the implementation of the sanitizer, this paper introduces a black-box learning algorithm that derives a Symbolic Finite Transducer (SFT). This black-box algorithm uses membership and equivalence oracles to derive such a model. In contrast to earlier research, SFTs not only describe the input or output language of a sanitizer but also how a sanitizer transforms the input into the output. As a result, we can reason about the transformations from input into output that are performed by the sanitizer. We have implemented this algorithm in an open-source tool of which we show that it can reason about the correctness of non-trivial sanitizers within a couple of minutes without any adjustments to the existing sanitizers. © Copyright 2020 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved.

Lecture Notes in Computer Science, 12229, ISSN:0302-9743, ISSN:1611-3349, NASA Formal Methods 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020, Proceedings, ISBN:978-3-030-55753-9, ISBN:978-3-030-55754-6

Lecture Notes in Computer Science, 12078, ISSN:0302-9743, ISSN:1611-3349, Tools and Algorithms for the Construction and Analysis of Systems. 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I, ISBN:978-3-030-45189-9, ISBN:978-3-030-45190-5

Already for many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief, and many individual success stories, no real change in industrial software development seems to happen. In fact, the software industry is moving fast forward itself, and the gap between what formal methods can achieve, and the daily software development practice does not seem to get smaller (and might even be growing).