Software developers often use logs to, e.g., investigate bugs, familiarize themselves with the underlying system, or improve performance. To do so, they commonly rely on text editors or their own scripts. This lack of appropriate tooling remains a primary challenge in the industrial application of log analysis (state-of-the-practice), despite many tools and techniques proposed by previous scientific studies (state-of-the-art). To aid in bridging this gap between industry and academia, between state-of-the-practice and state-of-the-art, we zoom in on the ways developers perform log analysis. In particular, we conduct an exploratory case study to understand what structures developers identify in logs and how they utilize their knowledge in this process. Based on the results of the case study, we identify two classes of features, one related to encoding domain knowledge and another one related to sharing domain knowledge. We implement two features from the first class in an open-source log analysis platform designed in collaboration with our industrial partner. To evaluate the impact of the implemented features on log analysis, we conduct a user evaluation with software developers from our industrial partner. During this evaluation developers complete several tasks using the features and complete a usability questionnaire. Results show that users are able to encode their domain knowledge about the logs during their analysis. Furthermore, we observe that participants value highly ease of use and indicate an interest in using the features in their current practice. This sentiment is reflected in the resulting scores of the usability questionnaire, indicating above-average usability. Our findings pave the way to bridge the gap between academia and industry and facilitate the application of advanced log analysis approaches in industry.

The high-tech industry is faced with ever growing amounts of software to be maintained and extended. To keep the associated costs under control, there is a demand for more human overview and for large-scale code restructurings. Language technology such as parsing can assist in this, but classical restructuring tools are typically not flexible enough to accommodate the needs of specific cases. In our research we investigate ways to make software restructuring tools customizable by software developers at Thermo Fisher Scientific as well as at other high-tech companies. We report on an industry-as-lab project, in which we have collaborated on cleaning up the compilation of COM interfaces of a large industrial software component. As a generic result, we have identified a method that we call model-based software restructuring. The approach taken is to extract high-level models from the code, use these to specify and visualize the restructuring, which is then translated into low-level code transformations. To implement this approach, we integrate generic technology to develop custom solutions. We aim for semiautomation and incrementally automate recurring restructuring patterns. The COM clean-up affected 72 type libraries and 1310 client projects with (one or more) dependencies on these type libraries. We have addressed these one type library at a time, and delivered all changes without blocking regular software development. Software developers in neighboring projects immediately noticed the very low defect rate of our restructuring. Moreover, as a spin-off, we have observed that the developed tools also start to contribute to regular software development.

No abstract available.

Abstraction is often essential to verify a program with model checking. Typically, a concrete source program with an infinite (or finite, but large) state space is reduced to a small, finite state, abstract program on which a correctness property can be checked. The fundamental question we investigate in this paper is whether such a reduction to finite state programs is always possible, for arbitrary branching time temporal properties. We begin by showing that existing abstraction frameworks are inherently incomplete for verifying purely existential or mixed universal-existential properties. We then propose a new, complete abstraction framework which is based on a class of focused transition systems (FTS's). The key new feature in FTS's is a way of "focusing" an abstract state to a set of more precise abstract states. While focus operators have been defined for specific contexts, this result shows their fundamental usefulness for proving non-universal properties. The constructive completeness proof provides linear size maximal models for properties expressed in logics such as CTL and the mu-calculus. This substantially improves upon known (worst-case) exponential size constructions for their universal fragments.

Abstract. A new notion, covering, generalising independence is introduced. It enables improved effects of partial-order reduction techniques when applied to real-time systems. Furthermore, we formulate a number of locally checkable conditions for covering that can be used as the basis for a practical algorithm. Correctness is proven with respect to a chosen discretisation method.

The advent of ever more complex reactive systems in increasingly critical areas calls for the development of automated verification techniques.Model checking is one such technique, which has proven quite successful.However, the state-explosion problem remains a major stumbling block.Recent experience indicates that solutions are to be found in the application of techniques for property-preserving abstraction and successive approximation of models.Most such applications have so far been based solely on the property-preserving characteristics of simulation relations.A major drawback of all these results is that they do not offer a satisfactory formalization of the notion of precision of abstractions.The theory of Abstract Interpretation offers a framework for the definition and justification of property-preserving abstractions.Furthermore, it provides a method for the effective computation of abstract models directly from the text of a program, thereby avoiding the need for intermediate storage of a full-blown model.Finally, it formalizes the notion of optimality, while allowing to trade precision for speed by computing suboptimal approximations.For a long time, applications of Abstract Interpretation have mainly focused on the analysis of universal safety properties, i.e., properties that hold in all states along every possible execution path.In this article, we extend Abstract Interpretation to the analysis of both existential and universal reactive properties, as expressible in the modal µ-calculus.It is shown how abstract models may be constructed by symbolic execution of programs.A notion of approximation between abstract models is defined while conditions are given under which optimal models can be constructed.Examples are given to illustrate this.We indicate conditions under which also falsehood of formulae is preserved.Finally, we compare our approach to those based on simulation relations.