Abstract Recursive state machines (RSMs)are state-based models for procedural programs with wide-ranging applications in program verification and interprocedural analysis. Model-checking algorithms for RSMs and related formalisms have been intensively studied in the literature. In this article, we devise a new model-checking algorithm for RSMs and requirements incomputation tree logic (CTL)that exploits the compositional structure of RSMs by ternary model checking in combination with a lazy evaluation scheme. Specifically, a procedural component is only analyzed in those cases in which it might influence the satisfaction of the CTL requirement. We implemented our model-checking algorithms and evaluate them on randomized scalability benchmarks and on an interprocedural data-flow analysis ofJavaprograms, showing both practical applicability and significant speedups in comparison to state-of-the-art model-checking tools for procedural programs.

Our university offers an IT-based design programme, with an engineering background in Computer Science and Electrical Engineering. Its focus on design and creativity, as well as the diversity of the students, requires an approach in informatics courses different from classical computer science programmes. While tinkering is an increasingly popular approach in STEM stimulation and education outside university, we argue that also in an academic setting a tinkering mindset has a relevant contribution. In this paper, we identify key elements in setting up tinkering sessions and report on their implementation for a course on algorithms. We will present and discuss results and observations of our teaching method, that are promising to continue and extend the tinkering approach in an academic setting

Abstract I have known Rob van Glabbeek as a colleague for 16 years, of which eight years were in the same research group. However, this only amounts to less than half of his professional life which started in the mid-1980s at the Centrum voor Wiskunde en Informatica in Amsterdam. In this article, I am trying to piece together the information I got from colleagues as well as from Rob himself—to the best of my recollection—to give an insight into Rob as a colleague, researcher, and person.

Most novice programmers write code that contains design smells which indicates that they are not understanding and applying important design concepts. This is especially true for students in degrees where programming, and by extension software design, is only a small part of the curriculum. This paper studies design smells in PROCESSING a language for new media and visual arts derived from Java. Language features - as well as common practices in the PROCESSING community - lead to language specific design smells. This paper defines design smells for PROCESSING, informed by a manual analysis of student code and community code. The paper describes how to detect these smells with static analysis. This serves two purposes, first to standardize design requirements, and second to assist educators with giving quality feedback. To validate its effectiveness we apply the tool to student code, community code, and code examples used by textbooks and instructors. This analysis also gives a good sense of common design problems in PROCESSING, their prevalence in novice code, and the quality of resources that students use for reference.

In this paper we present a rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using a formal specification in AWN (Algebra for Wireless Networks), a process algebra which has been specifically tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol correctness properties by providing a detailed proof of loop freedom. In contrast to evaluations using simulation or other formal methods such as model checking, our proof is generic and holds for any possible network scenario in terms of network topology, node mobility, traffic pattern, etc. A key contribution of this paper is the demonstration of how the reasoning and proofs can relatively easily be adapted to protocol variants.

Programming embedded system software typically involves more than one programming language. Normally, a high-level language such as C/C++ is used for application oriented tasks and a low-level assembly language for direct interaction with the underlying hardware. In most cases those languages are closely interwoven and the assembly is embedded in the C/C++ code. Verification of such programs requires the integrated analysis of both languages at the same time. However, common algorithmic verification tools fail to address this issue. In this work we present a model-checking based static analysis approach which seamlessly integrates the analysis of embedded ARM assembly with C/C++ code analysis. In particular, we show how to automatically check that the ARM code complies to its interface descriptions. Given interface compliance, we then provide an extended analysis framework for checking general properties of ARM code. We implemented this analysis in our source code analysis tool Goanna, and applied to the source code of an L4 micro kernel implementation.

Software has been under scrutiny by the verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness of and to eliminate bugs from such systems: software model checking and static analysis. Those approaches are typically complementary. In this paper we use a model checking approach to solve static analysis problems. This not only avoids the scalability and abstraction issues typically associated with model checking, it allows for specifying new properties in a concise and elegant way, scales well to large code bases, and the built-in optimizations of modern model checkers enable scalability also in terms of numbers of properties to be checked. In particular, we present Goanna, the first C/C++ static source code analyzer using the off-the-shelfmodel checker NuSMV, and we demonstrate Goanna's suitability for developer machines by evaluating its run-time performance, memory consumption and scalability using the source code of OpenSSL as a test bed.

Wireless networks consist of small (possibly) portable devices which combine battery-operated computing power and wireless communications. There are a number of technical challenges associated with their operation. These are addressed in part by emerging protocols which attempt to make trade-offs between the various network phenomena in order to optimise overall performance relative to an intended application. Central to the protocol design process is the availability of rigorous tools and techniques for quantifying any putative performance advantage gained by a particular protocol, and the degree to which its use degrades overall network functionality. The tools performing this important task today are simulators but the results from them are often not realistic as they have not been validated against empirical data (D. Cavin et al.). In this paper we explore the benefits of a formal approach to the analysis of wireless networks; in particular we investigate how a careful mix of model checking and proof may be used both to validate design decisions, and to provide a full profile of quantitative performance-style behaviours. Moreover the counterexample facility of model checking can illustrate clearly the limitations of some standard protocols. We demonstrate the methods on flooding and communications protocols.