arXiv subjects

Bertrand Meyer

Publications and source records attributed to Bertrand Meyer.

At least 37 records · Page 2Linked to original sources

arXiv2022

Improving Counterexample Quality from Failed Program Verification

In software verification, a successful automated program proof is the ultimate triumph. The road to such success is, however, paved with many failed proof attempts. The message produced by the prover when a proof fails is often obscure, making it very hard to know how to proceed further. The work reported here attempts to help in such cases by providing immediately understandable counterexamples. To this end, it introduces an approach called Counterexample Extraction and Minimization (CEAM). When a proof fails, CEAM turns the counterexample model generated by the prover into a a clearly understandable version; it can in addition simplify the counterexamples further by minimizing the integer values they contain. We have implemented the CEAM approach as an extension to the AutoProof verifier and demonstrate its application to a collection of examples.

cs.SE↗

arXiv2021

Class Invariants: Concepts, Problems, Solutions

Class invariants are both a core concept of object-oriented programming and the source of the two key open OO verification problems: furtive access (from callbacks) and reference leak. Existing approaches force on programmers an unacceptable annotation burden. This article explains invariants and solves both problems modularly through the O-rule, defining fundamental OO semantics, and the inhibition rule, using information hiding to remove harmful reference leaks. It also introduces the concept of "object tribe" as a basis for other possible approaches. For all readers: this article is long because it includes a tutorial, covers many examples and dispels misconceptions. To understand the key ideas and results, however, the first two pages suffice. For non-experts in verification: all concepts are explained; anyone with a basic understanding of object-oriented programming can understand the discussion. For experts: the main limitation of this work is that it is a paper proposal (no soundness proof, no implementation). It addresses, however, the known problems with class invariants, solving such examples as linked lists and Observer, through a simple theory and without any of the following: ownership; separation logic; universe types; object wrapping and unwrapping; semantic collaboration, observer specifications; history invariants; "inc" and "coop" constructs; friendship construct; non-modular reasoning. More generally, it involves no new language construct and no new programmer annotations.

cs.SE↗

arXiv2020

The role of formalism in system requirements (full version)

A major determinant of the quality of software systems is the quality of their requirements, which should be both understandable and precise. Most requirements are written in natural language, good for understandability but lacking in precision. To make requirements precise, researchers have for years advocated the use of mathematics-based notations and methods, known as "formal". Many exist, differing in their style, scope and applicability. The present survey discusses some of the main formal approaches and compares them to informal methods. The analysis uses a set of 9 complementary criteria, such as level of abstraction, tool availability, traceability support. It classifies the approaches into five categories: general-purpose, natural-language, graph/automata, other mathematical notations, seamless (programming-language-based). It presents approaches in all of these categories, altogether 22 different ones, including for example SysML, Relax, Eiffel, Event-B, Alloy. The review discusses a number of open questions, including seamlessness, the role of tools and education, and how to make industrial applications benefit more from the contributions of formal approaches. (This is the full version of the survey, including some sections and two appendices which, because of length restrictions, do not appear in the submitted version.)

cs.SE↗

arXiv2019

AutoFrame: Automatic Frame Inference for Object-Oriented Languages

Automatic program verification has made tremendous strides, but is not yet for the masses. How do we make it less painful? This article addresses one of the obstacles: the need to specify explicit "frame clauses", expressing what properties are left unchanged by an operation. It is fair enough to ask the would-be (human) prover to state what each operation changes, and how, but the (mechanical) prover also requires knowledge of what it does not change. The process of specifying and verifying these properties is tedious and error-prone, and must be repeated whenever the software evolves. it is also hard to justify, since all the information about what the code changes is in the code itself. The AutoFrame tool presented here performs this analysis entirely automatically. It applies to object-oriented programming, where the issue is compounded by aliasing: if x is aliased to y, any update to x.a also affects y.a, even though the updating instruction usually does not even mention y. This aspect turns out to be the most delicate, and is addressed in AutoFrame by taking advantage of a companion tool, AutoAlias, which performs sound and sufficiently precise alias analysis, also in an entirely automatic way. Some practical results of AutoFrame so far are: (1) the automatic reconstruction (in about 25 seconds on an ordinary laptop) of the exact frame clauses, a total of 169 clauses, for an 8,000-line data structures and algorithms library which was previously (with the manually written frame clauses) verified for functional correctness using a mechanical program prover; and (2) the automatic generation (in less than 4 minutes) of frame conditions for a 150,000-line graphical and GUI library. The source code of AutoFrame and these examples are available for download.

cs.SE↗

arXiv2019

The Anatomy of Requirements

Requirements engineering is crucial to software development but lacks a precise definition of its fundamental concepts. Even the basic definitions in the literature and in industry standards are often vague and verbose. To remedy this situation and provide a solid basis for discussions of requirements, this work provides precise definitions of the fundamental requirements concepts and two systematic classifications: a taxonomy of requirement elements (such as components, goals, constraints...) ; and a taxonomy of possible relations between these elements (such as "extends", "excepts", "belongs"...). The discussion evaluates the taxonomies on published requirements documents; readers can test the concepts in two online quizzes. The intended result of this work is to spur new advances in the study and practice of software requirements by clarifying the fundamental concepts.

cs.SE↗

arXiv2019

AutoAlias: Automatic Variable-Precision Alias Analysis for Object-Oriented Programs

The aliasing question (can two reference expressions point, during an execution, to the same object?) is both one of the most critical in practice, for applications ranging from compiler optimization to programmer verification, and one of the most heavily researched, with many hundreds of publications over several decades. One might then expect that good off-the-shelf solutions are widely available, ready to be plugged into a compiler or verifier. This is not the case. In practice, efficient and precise alias analysis remains an open problem. We present a practical tool, AutoAlias, which can be used to perform automatic alias analysis for object-oriented programs. Based on the theory of "duality semantics", an application of Abstract Interpretation ideas, it is directed at object-oriented languages and has been implemented for Eiffel as an addition to the EiffelStudio environment. It offers variable-precision analysis, controllable through the choice of a constant that governs the number of fix point iterations: a higher number means better precision and higher computation time. All the source code of AutoAlias, as well as detailed results of analyses reported in this article, are publicly available. Practical applications so far have covered a library of data structures and algorithms and a library for GUI creation. For the former, AutoAlias achieves a precision appropriate for practical purposes and execution times in the order of 25 seconds for about 8000 lines of intricate code. For the GUI library, AutoAlias produces the alias analysis in around 232 seconds for about 150000 lines of intricate code.

cs.SE↗

arXiv2019

AutoReq: expressing and verifying requirements for control systems

The considerable effort of writing requirements is only worthwhile if the result meets two conditions: the requirements reflect stakeholders' needs, and the implementation satisfies them. In usual approaches, the use of different notations for requirements (often natural language) and implementations (a programming language) makes both conditions elusive. AutoReq, presented in this article, takes a different approach to both the writing of requirements and their verification. Applying the approach to a well-documented example, a landing gear system, allowed for a mechanical proof of consistency and uncovered an error in a published discussion of the problem.

cs.SE↗

arXiv2017

Fourteen Years of Software Engineering at ETH Zurich

A Chair of Software Engineering existed at ETH Zurich, the Swiss Federal Insti-tute of Technology, from 1 October 2001 to 31 January 2016, under my leader-ship. Our work, summarized here, covered a wide range of theoretical and practi-cal topics, with object technology in the Eiffel method as the unifying thread .

cs.SE↗

arXiv2017

A contract-based method to specify stimulus-response requirements

A number of formal methods exist for capturing stimulus-response requirements in a declarative form. Someone yet needs to translate the resulting declarative statements into imperative programs. The present article describes a method for specification and verification of stimulus-response requirements in the form of imperative program routines with conditionals and assertions. A program prover then checks a candidate program directly against the stated requirements. The article illustrates the approach by applying it to an ASM model of the Landing Gear System, a widely used realistic example proposed for evaluating specification and verification techniques.

cs.SE↗

arXiv2017

Seamless Requirements

Popular notations for functional requirements specifications frequently ignore developers' needs, target specific development models, or require translation of requirements into tests for verification; the results can give out-of-sync or downright incompatible artifacts. Seamless Requirements, a new approach to specifying functional requirements, contributes to developers' understanding of requirements and to software quality regardless of the process, while the process itself becomes lighter due to the absence of tests in the presence of formal verification. A development case illustrates these benefits, and a discussion compares seamless requirements to other approaches.

cs.SE↗

arXiv2016

An Interference-Free Programming Model for Network Objects

Network objects are a simple and natural abstraction for distributed object-oriented programming. Languages that support network objects, however, often leave synchronization to the user, along with its associated pitfalls, such as data races and the possibility of failure. In this paper, we present D-SCOOP, a distributed programming model that allows for interference-free and transaction-like reasoning on (potentially multiple) network objects, with synchronization handled automatically, and network failures managed by a compensation mechanism. We achieve this by leveraging the runtime semantics of a multi-threaded object-oriented concurrency model, directly generalizing it with a message-based protocol for efficiently coordinating remote objects. We present our pathway to fusing these contrasting but complementary ideas, and evaluate the performance overhead of the automatic synchronization in D-SCOOP, finding that it comes close to---or outperforms---explicit locking-based synchronization in Java RMI.

cs.DC↗

arXiv2016

Unifying Requirements and Code: an Example

Requirements and code, in conventional software engineering wisdom, belong to entirely different worlds. Is it possible to unify these two worlds? A unified framework could help make software easier to change and reuse. To explore the feasibility of such an approach, the case study reported here takes a classic example from the requirements engineering literature and describes it using a programming language framework to express both domain and machine properties. The paper describes the solution, discusses its benefits and limitations, and assesses its scalability.

cs.SE↗

arXiv2016

Complete contracts through specification drivers

Existing techniques of Design by Contract do not allow software developers to specify complete contracts in many cases. Incomplete contracts leave room for malicious implementations. This article complements Design by Contract with a simple yet powerful technique that removes the problem without adding syntactical mechanisms. The proposed technique makes it possible not only to derive complete contracts, but also to rigorously check and improve completeness of existing contracts without instrumenting them.

cs.SE↗

arXiv2015

Theory of Programs

A general theory of programs, programming and programming languages built up from a few concepts of elementary set theory. Derives, as theorems, properties treated as axioms by classic approaches to programming. Covers sequential and concurrent computation.

cs.PL↗

arXiv2015

Contract-Based General-Purpose GPU Programming

Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adoption, however, is the difficulty of programming them and the low-level control of the hardware required to achieve good performance. This paper suggests a programming library, SafeGPU, that aims at striking a balance between programmer productivity and performance, by making GPU data-parallel operations accessible from within a classical object-oriented programming language. The solution is integrated with the design-by-contract approach, which increases confidence in functional program correctness by embedding executable program specifications into the program text. We show that our library leads to modular and maintainable code that is accessible to GPGPU non-experts, while providing performance that is comparable with hand-written CUDA code. Furthermore, runtime contract checking turns out to be feasible, as the contracts can be executed on the GPU.

cs.DC↗

arXiv2015

Efficient and Reasonable Object-Oriented Concurrency

Making threaded programs safe and easy to reason about is one of the chief difficulties in modern programming. This work provides an efficient execution model for SCOOP, a concurrency approach that provides not only data race freedom but also pre/postcondition reasoning guarantees between threads. The extensions we propose influence both the underlying semantics to increase the amount of concurrent execution that is possible, exclude certain classes of deadlocks, and enable greater performance. These extensions are used as the basis an efficient runtime and optimization pass that improve performance 15x over a baseline implementation. This new implementation of SCOOP is also 2x faster than other well-known safe concurrent languages. The measurements are based on both coordination-intensive and data-manipulation-intensive benchmarks designed to offer a mixture of workloads.

cs.DC↗

arXiv2015

On the Verification of SCOOP Programs

In this paper we focus on the development of a toolbox for the verification of programs in the context of SCOOP -- an elegant concurrency model, recently formalized based on Rewriting Logic (RL) and Maude. SCOOP is implemented in Eiffel and its applicability is demonstrated also from a practical perspective, in the area of robotics programming. Our contribution consists in devising and integrating an alias analyzer and a Coffman deadlock detector under the roof of the same RL-based semantic framework of SCOOP. This enables using the Maude rewriting engine and its LTL model-checker "for free", in order to perform the analyses of interest. We discuss the limitations of our approach for model-checking deadlocks and provide solutions to the state explosion problem. The latter is mainly caused by the size of the SCOOP formalization which incorporates all the aspects of a real concurrency model. On the aliasing side, we propose an extension of a previously introduced alias calculus based on program expressions, to the setting of unbounded program executions such as infinite loops and recursive calls. Moreover, we devise a corresponding executable specification easily implementable on top of the SCOOP formalization. An important property of our extension is that, in non-concurrent settings, the corresponding alias expressions can be over-approximated in terms of a notion of regular expressions. This further enables us to derive an algorithm that always stops and provides a sound over-approximation of the "may aliasing" information, where soundness stands for the lack of false negatives.

cs.SE↗

arXiv2014

Benchmarking Usability and Performance of Multicore Languages

Developers face a wide choice of programming languages and libraries supporting multicore computing. Ever more diverse paradigms for expressing parallelism and synchronization become available while their influence on usability and performance remains largely unclear. This paper describes an experiment comparing four markedly different approaches to parallel programming: Chapel, Cilk, Go, and Threading Building Blocks (TBB). Each language is used to implement sequential and parallel versions of six benchmark programs. The implementations are then reviewed by notable experts in the language, thereby obtaining reference versions for each language and benchmark. The resulting pool of 96 implementations is used to compare the languages with respect to source code size, coding time, execution time, and speedup. The experiment uncovers strengths and weaknesses in all approaches, facilitating an informed selection of a language under a particular set of requirements. The expert review step furthermore highlights the importance of expert knowledge when using modern parallel programming approaches.

cs.DC↗