Static program analysis refers to determining properties of programs without executing it, relying on a range of formal methods. While these methods have been around for a long time, over the last couple of years, some of these methods started to scale to solve problems of interesting size. We have used advanced type systems, abstract interpretation, SMT solving and model checking to answer relevant questions about programs written with various DSLs. In this booklet we introduce the methods, illustrate what we have done with them, and describe how we have integrated the analysis method and existing tools with languages and IDEs.
IncAL: A DSL for Incremental Program Analysis with Lattices
Tamás Szabó, Sebastian Erdweg, and Markus Völter.
In International Workshop on Incremental Computing (IC), 2017. [ pdf ]
We describe IncAL, a DSL for incremental lattice-based program analyses. IncAL is an extension of our previous work, IncA, which supported relational program analyses, that has been used for practically relevant analyses on industrial code bases. IncAL improves the expressive power of IncA by adding support for synthesis of data, enabling, for example, incremental execution of interval analysis.
Lessons learned from developing mbeddr: a case study in language engineering with MPS
Markus Völter, Bernd Kolb, Tamás Szabó, Daniel Ratiu, and Arie van Duersen.
In Software and Systems Modeling, 2016. [ pdf ]
Language workbenches are touted as a promising technology to engineer languages for use in a wide range of domains, from programming to science to business. However, not many real-world case studies exist that evaluate the suitability of language workbench technology for this task. This paper contains such a case study.
In particular, we evaluate the development of mbeddr, a collection of integrated languages and language extensions built with the Jetbrains MPS language workbench. mbeddr consists of 81 languages, with their IDE support, 34 of them C extensions. The mbeddr languages use a wide variety of notations – textual, tabular, symbolic and graphical – and the C extensions are modular; new extensions can be added without changing the existing implementation of C. mbeddr’s development has spanned 10 person years so far, and the tool is used in practice and continues to be developed. This makes mbeddr a meaningful case study of non-trivial size and complexity.
The evaluation is centered around five research questions: language modularity, notational freedom and projectional editing, mechanisms for managing complexity, performance and scalability issues and the consequences for the development process.
Dedicated Support for Analyses and Optimizations in Language Workbenches
In Proceedings of Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) - Doctoral Symposium, ACM, 2016. [ pdf ]
Language workbenches are widely used to implement domain-specific languages (DSLs) and their accompanying integrated development environments (IDEs). They help to define the abstract syntax, concrete syntax(es), type system, and transformations for the languages. However, there are other language aspects, specifically program analyses and optimizations, that are also crucial to a language implemen- tation, but state-of-the-art language workbenches has only limited support for them. The high implementation effort for these language aspects is justifiable for a general-purpose language (GPL), but is not justifiable for DSLs because of their different development economies.
To this end, I conduct research on dedicated support for analyses and optimizations for DSLs in language workbenches. My main goal is to develop declarative meta-languages that help to define static program analyses and that capture and automate patterns and techniques of optimizations. The research directions are directly driven by industrial need, and upon successful completion, the results would be applied in projects centered around DSLs for high-performance computing (HPC), insurance, and concurrent embedded systems.
Efficient Development of Consistent Projectional Editors using Grammar Cells
Markus Völter, Tamás Szabó, Sascha Lisson, Bernd Kolb, Sebastian Erdweg, and Thorsten Berger.
In Proceedings of Software Language Engineering (SLE), ACM, 2016. [ pdf ]
The definition of a projectional editor does not just specify the notation of a language, but also how users interact with the notation. Because of that it is easy to end up with different interaction styles within one and between multiple languages. The resulting inconsistencies have proven to be a major usability problem. To address this problem, we introduce grammar cells, an approach for declaratively specifying textual notations and their interactions for projectional editors. In the paper we motivate the problem, give a formal definition of grammar cells, and define their mapping to low-level editor behaviors. Our evaluation based on project experience shows that grammar cells improve editing experience by providing a consistent and intuitive, “text editor-like” user experience for textual notations. At the same time they do not limit language composability and the use of non-textual notations, the primary benefits of projectional editors. We have implemented grammar cells for Jetbrains MPS, but they can also be used with other projectional editors.
IncA: A DSL for the Definition of Incremental Program Analyses
Tamás Szabó, Sebastian Erdweg, and Markus Voelter.
In Proceedings of International Conference on Automated Software Engineering (ASE), ACM, 2016. [ pdf ]
Program analyses support software developers, for example, through error detection, code-quality assurance, and by enabling compiler optimizations and refactorings. To provide real-time feedback to developers within IDEs, an analysis must run efficiently even if the analyzed code base is large.
To achieve this goal, we present a domain-specific language called IncA for the definition of efficient incremental program analyses that update their result as the program changes. IncA compiles analyses into graph patterns and relies on existing incremental matching algorithms. To scale IncA analyses to large programs, we describe optimizations that reduce caching and prune change propagation. Using IncA, we have developed incremental control flow and points-to analysis for C, well-formedness checks for DSLs, and 10 FindBugs checks for Java. Our evaluation demonstrates significant speedups for all analyses compared to their non-incremental counterparts.
An Extensible Framework for Variable-Precision Data-Flow Analyses in MPS
Tamás Szabó, Simon Alperovich, Markus Voelter, and Sebastian Erdweg.
In Proceedings of International Conference on Automated Software Engineering (ASE) - Tool Track, ACM, 2016. [ pdf ]
Data-flow analyses are used as part of many software engineering tasks: they are the foundations of program understanding, refactorings and optimized code generation. Similar to general-purpose languages (GPLs), state-of-the-art domain-specific languages (DSLs) also require sophisticated data-flow analyses. However, as a consequence of the different economies of DSL development and their typically relatively fast evolution, the effort for developing and evolving such analyses must be lowered compared to GPLs. This tension can be resolved with dedicated support for data-flow analyses in language workbenches.
In this tool paper we present MPS-DF, which is the component in the MPS language workbench that supports the definition of data-flow analyses for DSLs. Language developers can define data-flow graph builders declaratively as part of a language definition and compute analysis results efficiently based on these data-flow graphs. MPS-DF is extensible such that it does not compromise the support for language composition in MPS. Additionally, clients of MPS-DF analyses can run the analyses with variable precision thus trading off precision for performance. This allows clients to tailor an analysis to a particular use case.
mbeddr: Extensible Languages for Embedded Software Development
Tamás Szabó, Markus Voelter, Bernd Kolb, Daniel Ratiu, Bernhard Schaetz.
In Proceedings of High Integrity Language Technology (HILT), ACM, 2014. [ pdf ]
In this industrial presentation we will demonstrate mbeddr, an extensible set of integrated languages for embedded software development. After discussing the context of the talk, we will give details about the mbeddr architecture, which relies on the MPS language workbench. Then, we will elaborate on the extension modules and show how they fit with safety-critical development processes. Finally, we will point out how the existing languages can be extended by the user by giving some real-world examples, including a language construct that could have prevented the Apple “goto fail” bug as well as mathematical notations.
Developing and Visualizing Live Model Queries
Zoltán Újhelyi, Tamás Szabó, István Ráth, Dániel Varró.
In Proceedings of Analysis of Model Transformations (AMT), ACM, 2012. [ pdf ]
Several important tasks performed by model driven development tools — such as well-formedness constraint validation or model transformations — rely on evaluating model queries. If the model changes rapidly or frequently, it is beneficial to provide live queries that automatically propagate these model changes into the query results. To ease the development and debugging of live queries, the development environment should provide a way to evaluate the query results continuously, helping to understand how the created query works.
This paper presents a generic live model query visualizer that displays and updates the query results depending on their source models. It has been implemented for the EMF-IncQuery framework and presented here for validating BPMN models.
Incremental pattern matching for the efficient computation of transitive closure
Gábor Bergmann, István Ráth, Tamás Szabó, Paolo Torrini, Dániel Varró.
In Proceedings of International Conference on Graph Transformations (ICGT), Springer-Verlag, 2012. [ pdf ]
Pattern matching plays a central role in graph transformations as a key technology for computing local contexts in which transformation rules are to be applied. Incremental matching techniques offer a performance advantage over the search-based approach, in a number of scenarios including on-the-fly model synchronization, model simulation, view maintenance, well-formedness checking and state space traversal. However, the incremental computation of transitive closure in graph pattern matching has started to be investigated only recently. In this paper, we propose multiple algorithms for the efficient computation of generalized transitive closures. As such, our solutions are capable of computing reachability regions defined by simple graph edges as well as complex binary relationships defined by graph patterns, that may be used in a wide spectrum of modeling problems. We also report on experimental evaluation of our prototypical implementation, carried out within the context of a stochastic system simulation case study.
Parallel Saturation Based Model Checking
András Vörös, Tamás Szabó, Attila Jámbor, Dániel Darvas, Ákos Horváth, Tamás Bartha.
In Proceedings of International Symposium on Parallel and Distributed Computing (ISPDC), IEEE, 2011. [ pdf ]
Formal verification is becoming a fundamental step of safety-critical and model-based software development. As part of the verification process, model checking is one of the current advanced techniques to analyze the behavior of a system. In this paper, we examine an existing parallel model checking algorithm and we propose improvements to eliminate some computational bottlenecks. Our measurements show that the resulting new algorithm has better scalability and performance than both the former parallel approach and the sequential algorithm.