title: Trellis: A Domain-Specific Language for Hidden Markov Models with Sparse Transitions

authors:
Lars Hummelgren
Viktor Palmkvist
Linnea Stjerna
Xuechun Xu
Joakim Jaldén
David Broman

abstract: Hidden Markov models (HMMs) are frequently used in areas such as speech recognition and bioinformatics. However, implementing HMM algorithms correctly and efficiently is time-consuming and error-prone. Specifically, using model-specific knowledge to improve performance, such as sparsity in the transition probability matrix, ties the implementation to a particular model, making it harder to modify. Previous work has introduced high-level frameworks for defining HMMs, thus lifting the burden of efficiently implementing HMM algorithms from the user. However, existing tools are ill-suited for sparse HMMs with many states. This paper introduces Trellis, a domain-specific language for succinctly defining sparse HMMs that use GPU acceleration to achieve high performance. We show that Trellis outperforms previous work and is on par with a hand-written CUDA kernel implementation for a particular sparse HMM.


venue: sle

title: AI Effects on Research and Education: A Programming and Software Language Perspective (Panel)

abstract: In this panel, we discuss how AI is affecting research and education in the field of programming and software languages. We explore different positions regarding carefully welcoming AI into research and education. We focus more on fundamental, philosophical, methodological questions, less so on specific technological advances or studies.


title: DSLs in Racket: You Want It How, Now?

authors:
Yunjeong Lee
Kiran Gopinathan
Ziyi Yang
Matthew Flatt
Ilya Sergey

abstract: Domain-Specific Languages (DSLs) are a popular way to simplify and streamline programmatic solutions of commonly occurring yet specialized tasks. While the design of frameworks for implementing DSLs has been a popular topic of study in the research community, significantly less attention has been given to studying how those frameworks end up being used by practitioners and assessing utility of their features for building DSLs "in the wild". In this paper, we conduct such a study focusing on a particular framework for DSL construction: the Racket programming language. We provide (a) a novel taxonomy of language design intents enabled by Racket-embedded DSLs, and (b) a classification of ways to utilize Racket's mechanisms that make the implementation of those intents possible. We substantiate our taxonomy with an analysis of 30 popular Racket-based DSLs, discussing how they make use of the available mechanisms and accordingly achieve their design intents. The taxonomy serves as a reusable measure that can help language designers to systematically develop, compare, and analyze DSLs in Racket as well as other frameworks.


title: Concrete Syntax Metapatterns

authors:
Luka Miljak
Casper Bach Poulsen
Rosilde Corvino

abstract: Software engineers should be able to apply massive code refactorings to maintain large legacy code bases. A key aspect of developing restructurings is matching and transforming code snippets using abstract syntax trees (ASTs). Matching on ASTs is typically done through AST patterns with holes. AST patterns can be extended to become metapatterns, which increase their expressivity. Metapattern examples include disjunctions, descendant patterns, and patches where we inline transformations into the pattern itself. Despite their expressivity, abstract syntax (meta)patterns can become verbose and require restructuring engineers to be intimately familiar with the data types that define the AST. A better approach is to use concrete syntax patterns, which allows us to denote our patterns in the syntax of the object language. Previous work has shown that we can use external black-box parsers of the object language to compile concrete syntax patterns for arbitrary languages. In this paper, we scale this compilation method to support concrete syntax metapatterns, which allows for a more declarative way of expressing restructurings. We evaluate this method through an implementation written in Kotlin.


title: Towards an In-Context LLM-Based Approach for Automating the Definition of Model Views

authors:
James William Pontes Miranda
Hugo Bruneliere
Massimo Tisi
Gerson Sunyé

abstract: In the Model-Driven Engineering (MDE) of complex systems, multiple models represent various systems' aspects. In practice, these models are often unconnected and specified using different modeling languages. Model view solutions can be employed to automatically combine such models. However, writing model view definitions is not trivial. When modeling languages are semantically distant and/or have a large number of concepts, it can quickly become difficult to manually identify the language elements to be selected, associated, or queried to build a model view. As a solution, this paper proposes an in-context Large Language Model (LLM)-based approach to assist engineers in writing model-view definitions. Notably, we rely on LLMs and Prompt Engineering techniques to automatically generate drafts of model-view definitions by providing as input only minimal information on the modeling languages to be combined. We implemented our approach by integrating the EMF Views solution for model views with the LangChain framework for LLM-based applications. To this end, we tailored LangChain to handle EMF metamodels. We validated our approach and implementation on a set of model views originally specified either in VPDL, the ViewPoint Definition Language of EMF Views, or as ATL model-to-model transformations. We compared these original model view definitions with the ones we automatically generated. The obtained results show the feasibility and applicability of our approach.


title: Type Checking with Rewriting Rules

abstract: Type classes support the implementation of highly reusable algorithms and data structures without loss of efficiency. Initially developed in Haskell, they have become central to the design of several modern programming languages, including Swift, Rust, Hylo, and Carbon. A key part of their success is the ability to express sophisticated abstractions using constraints on the types associated with their operations. However, this expressiveness invites thorny theoretical and engineering questions. In particular, the support of recursive constraints—i.e., constraints specifying that an associated type of an abstraction must be a model of that abstraction—leaves type equivalence undecidable. This paper studies a semi-decidable technique to tackle this problem that was first developed in Swift’s compiler. The core idea is to encode constraints into a term rewriting system and use normalization to answer type checking queries. We describe this approach formally through the lens of , a calculus originally designed to capture generic programming best practices; and discuss an implementation in the context of Hylo, a language inspired by Swift and Rust.


title: Method Bundles

authors:
Dimi Racordon
Dave Abrahams

abstract: Performance-critical systems commonly optimize memory use and locality by selecting among multiple variants of a single logical operation. Algorithm developers then typically rely on ad-hoc API patterns or naming conventions to distinguish the variants. Unfortunately, this practice suffers from poor ergonomics. Users are compelled to understand the conventions and carefully consider the signatures and documentation of different variants, which creates drag on development and maintenance. Instead, we propose a language construct bundling algorithm variants having well-defined semantic relationships under a single name. This approach eliminates boilerplate, reduces cognitive overhead by consolidating APIs, and unlocks compiler optimizations.


title: Aconite: Towards Generating Sirius-Based Graphical Editors from Annotated Metamodels

authors:
Nathan Richardson
Dimitris S. Kolovos
Antonio García-Domínguez

abstract: Sirius is a powerful framework for implementing graphical editors for modelling languages. Sirius can help manage model complexity by presenting the same model through multiple notations ("viewpoints" in Sirius), dedicated to different audiences and/or tasks. However, this flexibility comes at the expense of having to manually define the mapping between each viewpoint and the metamodel. This paper explores a textual notation to efficiently annotate a metamodel with such a mapping, and transform the metamodel into one or more Sirius viewpoint descriptors, with the aim to reduce the manual work required to produce and maintain Sirius-based graphical notations. We present Aconite, an open-source tool which implements this approach, and demonstrate it through the re-implementation of a common Sirius example notation, and a simplified version of a BPMN editor. Aconite includes mechanisms for automated generation of navigation expressions in common scenarios, and for inheritance of graphical styles to reduce repetition.


title: Efficient Demand Evaluation of Fixed-Point Attributes using Static Analysis

authors:
Idriss Riouak
Niklas Fors
Jesper Öqvist
Görel Hedin
Christoph Reichenbach

abstract: Declarative approaches to program analysis promise a number of practical advantages over imperative approaches, from eliminating manual worklist management to increasing modularity. Reference Attribute Grammars (RAGs) are one such approach. One particular advantage of RAGs is the automatic generation of on-demand implementations, suitable for query-based interactive tooling as well as for client analyses that do not require full evaluation of underlying analyses. While historically aimed at compiler frontend construction, the addition of circular (fixed-point) attributes also makes them suitable for dataflow problems. However, prior algorithms for on-demand circular RAG evaluation can be inefficient or even impractical for dataflow analysis of realistic programming languages like Java. We propose a new demand algorithm for attribute evaluation that addresses these weaknesses, and apply it to a number of real-world case studies. Our algorithm exploits the fact that some attributes can never be circular, and we describe a static meta-analysis that identifies such attributes, and obtains a median steady-state performance speedup of ~2.5x and ~22x for dead-assignment and null-pointer dereference analyses, respectively.


title: Cloud Programming Languages and Infrastructure from Code: An Empirical Study

authors:
Georg Simhandl
Uwe Zdun

abstract: Infrastructure-from-Code (IfC) is a new approach to DevOps and an advancement of Infrastructure-as-Code (IaC). One of its key concepts is to provide a higher level of abstraction facilitated by new programming languages or software development kits, which automatically generate the necessary code and configurations to provision the infrastructure, deploy the application, and manage the cloud services. IfC approaches promise higher developer productivity by reducing DevOps-specific tasks and the expert knowledge required. However, empirical studies on developers' performance, perceived ease of use, and usability related to IfC are missing. We conducted a controlled experiment (n=40) to assess the usability of the cloud programming languages (PL) and software development kits (SDK). Both approaches involve similar effectiveness. We found that the PL-based approach was moderately less efficient but increased correctness with time spent on programming. Tracing generated infrastructure configurations from code was more challenging with the SDK-based approach. Applying thematic analysis, 19 themes emerged related to usability barriers, supporting factors, security, cloud cost, and enhancement areas. We conclude with five findings and future directions.


title: The Linguistic Theory behind Blockly Languages

authors:
Friedrich Steimann
Robin Stunic

abstract: The dominant linguistic theory for specifying the syntax of software languages is Chomsky's phrase-structure grammar. However, for graphical block languages (such as Scratch and other languages defined using Google's Blockly library), we note that a different linguistic theory provides a better fitting model: the theory of dependency grammar. Indeed, as we make clear, there is a close, almost one-to-one correspondence between the specifications of graphical syntax required by Blockly and a classic capture of dependency grammar, which can be perfected by making only small extensions that remain entirely within the linguistic context. Taking the identified correspondence further suggests how Blockly languages can become context-sensitive, a requirement of many software languages that so far, Blockly addresses only in ad hoc ways.


title: Design of Software Representation Languages: A Historical Perspective

abstract: The history of software development includes numerous tex- tual and graphical ways to represent software structures and the mechanisms for executing high-level instructions. The proliferation of programming languages is a visible outcome of that effort, with many popular languages having a strong association with their creator(s). In this paper, we present a historically focused overview of many different types of software representations, primarily programming languages, but also graphical notations that can generate code in a programming language or be directly executed with associated tools. The paper then describes some of the characteristics that differentiate them from one another, and concludes with a review of guidelines for designing programming languages and notations.


title: Reducing Write Barrier Overheads for Orthogonal Persistence

authors:
Yilin Zhang
Omkar Dilip Dhawal
V. Krishna Nandivada
Shigeru Chiba
Tomoharu Ugawa

abstract: Orthogonal persistence implemented with non-volatile memory (NVM) allows the programmers to easily create persistent containers, which are container data-structures preserved even after the process terminations due to a system crash. However, the state-of-the-art technique of its implementation in multithreaded languages rely on the instruction, which limits out-of-order execution. This overhead is applied regardless of the use of persistent objects. We propose a technique that does not disturb out-of-order execution. Instead, we let the thread that is attempting to make an object persistent synchronize with all the other threads by handshaking. Furthermore, we propose a technique to eliminate the redundancy of that synchronization by a novel static analysis called persistence-aware escape analysis. We implemented both the proposed techniques in RBP (replication based persistency) implemented in the HotSpot VM of OpenJDK. As a result of our evaluation, we observed that the execution speed was faster than RBP by 23.0objects, and it was only 10.6which does not support orthogonal persistence. When a program used persistent objects, execution speed was almost the same as RBP. These results demonstrate that orthogonal persistence using NVM can be implemented in a practical way.


title: Dynamic Dependency-Based Purity Checking

authors:
Anton Risberg Alaküla
Niklas Fors
Christoph Reichenbach

abstract:
Many software language tools use declarative domain-specific languages (DDSLs) to implement parts of their functionality, such as context-free grammars for parsing or inference rules for type analysis. For interoperability and ease of use, DDSLs often rely on embedded general-purpose language (GPL) code fragments, as in the semantic actions of parser specifications, but require that these GPL fragments fulfill certain semantic properties, such as the absence of observable side effects. Fulfilling these properties is usually up to the developer, and accidental violations can lead to subtle and hard-to-trace bugs.

We present Tragdor, a tool that dynamically checks for property violations in Reference Attribute Grammars (RAGs) written for the JastAdd metacompiler, and report on the efficacy of four property testing strategies that Tragdor employs. Even in a mature RAG like the Java 11 compiler ExtendJ, Tragdor was able to find 13 implementation issues, 2 of which we consider to be of high severity. Our manual inspection of Tragdor's reports identifies a number of potential RAG anti-patterns and finds evidence that the inherent dependency structure of RAGs often encodes fine-grained implicit contracts.


title: A New DSL Textbook in Town!

abstract:
DSLs are the ultimate abstraction in software engineering. While programming languages have --- since the advent of computers --- continuously increased their level of abstraction, they are still limited to the domain of computing, with their instances containing many technicalities. Unlike programming languages, DSLs reflect a given application domain, ideally abstracting away anything beyond it. Recognizing their strengths, the programming-language and the software engineering community introduced many technologies for engineering DSLs. While well-polished widely-used DSLs have existed for a long time (e.g., SQL, regular expressions, HTML), language engineering technologies have made great progress over the last two decades, allowing developers who are not language or compiler experts to create their own DSL --- in order to increase the level of automation for their projects.

In the keynote, I will report on our decade of experiences from teaching DSL engineering. I will especially present our recent book [1]. Andrzej Wąsowski and I wrote it to:

• establish more of an engineering perspective for creating DSLs, teaching the problem-oriented creation of DSLs and different engineering activities including testing and requirements (domain analysis);

• bring the programming language and software engineering community together by teaching solutions from both fields --- many of which overlap conceptually --- and thereby unifying and integrating them;

• demonstrate how to use a modern functional and object-oriented language, Scala, to engineer internal and external DSLs, while not limiting the presentation to a single programming language

• provide a large number of exercises (277 in total) for effective learning, like mathematics textbooks do; and

• contribute a large number of examples where DSLs are effective, with a whole chapter on DSLs for creating software platforms (a.k.a. product lines).


title: Scheduling the Construction and Interrogation of Scope Graphs Using Attribute Grammars

authors:
Luke Bessant
Eric Van Wyk

abstract:
Recognizing that name binding is often done in an ad-hoc manner, Visser and his colleagues introduced scope graphs as a uniform representation of a program's static binding structure along with a generic means for interrogating that representation to resolve name references to their declarations. A challenge arises in scheduling the construction and querying actions so that a name resolution is not performed before all requisite information for that resolution is added to the scope graph. Visser et al. introduced a notion of weakly critical edges to constrain the order in which name resolution queries are performed to a correct one, but this has been found to be somewhat restrictive.

Visser et al. also introduced Statix, a constraint solving language for scope graph-based name resolution. We show that specifications written in an annotated version of Statix can be translated into reference attribute grammars, and that the order in which equations are solved under demand driven evaluation provides a valid order for solving constraints in Statix. This formalizes what has been folklore in the attribute grammar community for some time, that scope graphs are naturally specified in reference attributes grammars.


title: Boosting Parallel Parsing through Cyclic Operator Precedence Grammars

authors:
Michele Chiari
Michele Giornetta
Dino Mandrioli
Matteo Pradella

abstract: Deterministic parsing of tree-structured data is usually performed sequentially left-to-right. Recently however, also motivated by the need to process extremely large data sets, a parallel version thereof has been devised which, thanks to the theoretical features of operator precedence languages (OPL) particularly well-suited to split the input into separate chunks, provided high improvements w.r.t. traditional sequential parsing. Further investigation pointed out a restriction imposed on the OPL formalism that prevents from fully exploiting parallelism and proposed an improvement of the original algorithm which proved effective in many practical cases. Stimulated by the above contribution here we remove the mentioned restriction on OPL and build a new parallel parser generator based thereon. We conducted a comparative experimentation among the three parallel algorithms that showed a consistent further improvement w.r.t. both the previous ones (with an exception in the case of purely sequential execution). Based on these early results, we believe that the horizon of parallel parsing large tree-structured data promises dramatic gains of efficiency in the analysis of this fundamental data structure.


title: Variability Fault Localization by Abstract Interpretation and its Application to SPL Repair

abstract:
Fault localization is an important step in software debugging that aims to isolate and localize the bugs (errors) to a small part of the program. This becomes more challenging in Software Product Lines (SPLs) due to the variable nature of bugs (so-called variability bugs). This paper introduces a novel variability fault localization algorithm for SPLs. Moreover, we present its practical application for automatic repair of variability bugs in SPLs.

Given a buggy SPL (program family) and an assertion to be satisfied, our variability fault localization algorithm infers so-called lifted (variability-specific) error invariants in all locations, which over-approximate the reachable states at the given locations that may produce the bug if the execution continues from those locations in some particular variants. The lifted error invariants are used for statement-wise lifted semantic slicing of buggy SPLs, which removes the statements irrelevant for assertion violation in certain variants containing some combinations of features. Finally, the obtained slice family is applied for designing an efficient SPL repair algorithm, which repeatedly mutates the (feature and program) expressions in the statements identified as relevant for the variability bug until a correct SPL is found.

We have implemented an experimental tool for variability fault localization and repair of #ifdef-annotated SPLs written in C. We have evaluated our approach on a set of benchmarks, and the experimental results confirm the effectiveness of our approach.


title: Integrating Model Checking into a Live Modeling Environment

authors:
Joeri Exelmans
Ciprian Teodorov
Hans Vangheluwe

abstract: Live modeling is the ability to change an executable model at runtime, and without having to restart its execution. Sometimes this 'breaks' the ongoing execution, but in many cases, it does not have to. In earlier work, we reduced this problem to detecting fine-grained read/write conflicts between the recorded history of edit operations (created by the user) and execution steps (created by the interpreter). In this paper, we extend our approach by adding the ability to perform model checking during live modeling sessions. We motivate that this further enhances the live modeling experience, producing counter-examples or 'witness traces' relative to the current execution state, as a possible 'future', integrated with the execution and edit history, minimizing the mental gap. The model checker itself is generic, and uses (via an adapter) the language's existing interpreter. This way, we could implement this paper's running example in a working prototype with relatively little effort.


title: TranspileJS, an Intelligent Framework for Transpiling JavaScript to WebAssembly

authors:
José Pedro Ferreira
João Bispo
Susana Lima

abstract: WebAssembly (Wasm) has emerged as a powerful binary format, enabling the seamless integration of languages like C and Rust into web applications. JavaScript (JS), the dominant language for client-side web development, has its code susceptible to tampering and intellectual property theft due to its transparency in browser environments. We introduce TranspileJS, a novel tool designed to enhance code security by automatically selecting and translating JS snippets into Wasm. TranspileJS leverages a multi-stage architecture that converts JS to TypeScript, which is compiled into Wasm using the AssemblyScript compiler. TranspileJS addresses the challenges posed by the fundamental differences between JS and Wasm, including dynamic typing, runtime behaviour mismatches, and standard library discrepancies, ensuring that the original behaviour of the code is preserved while maximising the amount of code transpiled. Our experiments show that TranspileJS successfully transpiles approximately one-third of the code in our dataset, with a performance impact of up to a 12.3% increase in execution time. The transpilation process inherently obfuscates code, creating effects similar to standard obfuscation techniques, and generates a stealthy and resilient output. Furthermore, combining transpilation with WebAssembly-specific obfuscation techniques opens new possibilities for code protection and resistance against reverse engineering.


title: Exploratory, Omniscient, and Multiverse Diagnostics in Debuggers for Non-Deterministic Languages

authors:
Damian Frölich
Tommaso Pacciani
L. Thomas van Binsbergen

abstract:
Debugging non-deterministic programs is inherently difficult as the compound effects of non-deterministic execution steps is hard to predict and gives rise to a (potentially) vast space of reachable program states such that manual exploration of all reachable states is infeasible.

Multiverse debugging addresses these problems by realising a fine-grained, exhaustive and interactive process for state space exploration. At SLE2023, Pasquier et al. presented a generic framework that makes exploration practical through user-defined reductions on program states and by proposing expressive logics for defining and searching for states and traces of interest, generalising the concept of breakpoint. The framework has been validated through the case study language AnimUML designed to make non-deterministic UML specifications executable.

In this paper, we perform additional case studies to evaluate the applicability of the framework. We analyse three non-deterministic, domain-specific languages representing three different domains: grammar engineering, formal operational semantics, and norm engineering. The framework is evaluated against requirements extracted from these domains, resulting in the identification of several limitations of the framework. We then propose a modified and extended framework and apply it to develop multiverse debuggers for the case study languages. The result demonstrates a multiverse debugging framework with more general applicability.


title: Optimize Effect Handling for Tail-resumption with Stack Unwinding

authors:
Yuze Fu
Shigeru Chiba

abstract: Algebraic effect handling is a superior abstraction for non-local control flows, unifying over the existing non-local control flow constructs such as try/catch, destructors, shared state, async/await and generators. To encourage the adoption of effect handlers, improving their performance is essential. Despite having a number of implementations, they lack enough focus on tail resumptive handlers which leaves space for an improvement. We believe that tail resumptive handlers are invoked more frequently and contributes more to the overall performance of programs. The characteristic of them implies the possibility of an implementation with little overhead over function invocation. We propose eff-unwind, an implementation of effect handling as a C++ library which is optimized for tail resumptive handlers at the cost of others. Our implementation uses function calling and returning for tail resuming for improved efficiency while using stack copying and setjmp for general resuming and stack unwinding for yielding. It eliminates the need of recomposing the stack or preserving memory in the lifecycle of a tail resumptive handler at the cost of a less efficient yielding and not-tail resuming. Additionally, our library exposes a functional interface and executes C++ destructors. We evaluate our approach based on a total of 12 cases containing both tail resumptive handlers and others. The result shows performance improvement for tail resuming and slowdown for others. We also discover that multishot handlers presents challenges with C++ destructors.


title: A Model-Driven Approach to Design, Generation, and Deployment of GUI Component Libraries

authors:
Arkadii Gerasimov
Nico Jansen
Judith Michael
Bernhard Rumpe
Sebastian Will

abstract: The reusability of modular, embeddable components is a key determinant for the success of modern programming languages to ensure efficient and high-quality development. However, there is a gap in the field of domain-specific modeling regarding reusable components at the model level. While libraries are relatively common and a de facto standard for prominent programming languages, establishing model libraries is still in its infancy. This paper specifies building a model-driven component library that utilizes a self-extension mechanism. We demonstrate an approach to structure, build, and integrate such a library using a wide range of GUI components, from essential atomic elements and more complex composed components to specifically tailored ones for particular application domains. Employing such libraries at the model level further supports the goal of model-driven engineering to assist domain experts in efficiently building high-quality systems.


title: (Semantic) Feature Model Differences with (Q)SAT

authors:
Simone Heisinger
Maximilian Heisinger
Martina Seidl

abstract: Feature models evolve in multiple iterations over time. When modellers change a model, they enact syntactical changes in order to produce specific semantic differences between model iterations. Many tools have been developed to analyze such syntactical differences, but the changing semantics of models were harder to assess. Tools for semantic differences between feature model iterations rely on Binary Decision Diagrams (BDDs) or encode each change into SAT, the former leading to BDD scaling issues and the latter requiring editor support or other specialized tooling. We contribute the first concise formalization of feature models and their semantic differences into propositional logic and use it to efficiently and scalably classify semantic differences using SAT solvers. We then extend our definition into QSAT in order to quantify the full list of semantic differences between feature models and enumerate them using QBF tools, without needing specialized feature model solvers. We implement a semantic difference classifier using our UVL processing pipeline based on Booleguru (instead of the more widely used FeatureIDE) and evaluate it on industrial feature model instances in the standardized UVL format. We also evaluate our QSAT-based semantic difference enumerator and reproduce prior results. We provide all software and evaluation results in an artifact.


title: AnyText: Incremental, left-recursive Parsing and Pretty-Printing from a single Grammar Definition with first-class LSP support

authors:
Georg Hinkel
Alexander Hert
Niklas Hettler
Kevin Weinert

abstract: Many current language workbenches do not support incremental parsing or left recursion, lack support for resolving references and pretty-printing or make it difficult to implement the Language Server Protocol (LSP) based on the generated parser. In this paper, we present AnyText, a new language workbench that solves these challenges by implementing the LSP using a scannerless, incremental packrat parser with support for left recursion, based on a grammar description in an extended EBNF-like grammar similar to Xtext/Langium. Furthermore, we show how an EBNF extension with formatting instructions can be used to obtain a pretty-printer. We use a combination of an internal and an external DSL to simplify the process of creating a new language. We demonstrate our approach using two new DSLs and evaluate performance and the amount of manual code necessary to support different editor features.


title: Lessons Learned from Developing the MontiCore Language Workbench: Challenges of Modular Language Design

authors:
Nico Jansen
Alex Lüpges
Bernhard Rumpe

abstract: In software language engineering, composition and modular design are essential milestones to advance reuse in this domain. Although language engineering improves quality and development efficiency by incorporating reusable components and tooling, some disadvantages and limitations can inhibit sophisticated language development. Current research usually focuses on the conceptual advantages but neglects the often technical drawbacks resulting from the necessity for complex interactions for seamless integration. In this paper, we report on our experiences applying language composition with the language workbench MontiCore and elaborate on the conceptual and technical drawbacks of the intended compositional tooling. Using concise application examples, we demonstrate the challenges of a compositional parser, the complexity of the generated infrastructure, and how they scrape the limits of the underlying target programming languages and their compilers. This critical examination of the implications of modular language construction demonstrates the pitfalls of language composition in the large and should reveal potential for future research.


title: Property-based Testing of Attribute Grammars

authors:
José Nuno Macedo
Marcos Viera
João Saraiva

abstract:
Software testing is an integral part of modern software development. Testing frameworks are part of the toolset of any software language allowing programmers to test their programs in order to detect bugs. Unfortunately, there is no work on testing in attribute grammars.

In this paper we combine the powerful property-based testing technique with the attribute grammar formalism. In such property-based attribute grammars, properties are defined on attribute instances. Properties are tested on large sets of randomly generated (abstract syntax) trees by evaluating their attributes.

We present an implementation that relies on strategies to express property-based attribute grammars. Strategies are tree-based recursion patterns that are used to encode logic quantifiers defining the properties.


title: Optimal Language Design is Hard: A Case Study in ECMAScript (JavaScript) Standardization

authors:
Philipp Riemer
Yury Nikulin
Ashley Claymore
Mikhail Barash

abstract:
In addition to requirements of a purely technical nature, the evolution of widely adopted programming languages is often governed by preferences of individual members---either persons or organizations---of the language maintenance team, who may associate issues with particular design aspects. For example, when adding a new primitive data type to a language, language designers may suggest alternative semantics for equality to existing data types, as well as explicitly specify issues they wish to avoid (such as inconsistent behavior among number-like types). The decision-making process can span over multiple years and can be highly unstructured, and in a dynamic and distributed language design team, the cumulated understanding of previously discussed design alternatives can thus be lost over time.

In this paper, we present a domain-specific language to specify a certain kind of language evolution proposals--- where the design space can be presented as a collection of interconnected individual design points. With each design point, one can associate a set of issues it could raise that should be avoided. From a DSL specification, an interactive web-based tool is generated that allows exploring the design space of a proposal.

Further assigning weights to issues, we formulate an optimization problem where the goal is to select alternatives for individual design points to minimize the total weight of occurring issues. We prove that this optimization problem is NP-hard. We reduce this problem to an integer linear programming problem and incorporate a solver into our interactive tool. We demonstrate the feasibility of our approach by using our DSL to specify the ECMAScript proposal Records & Tuples, and demonstrate that any design choice---as described in the proposal---will necessarily raise issues.


title: Detecting Resource Leaks on Android with Alpakka

authors:
Gustavo Santos
João Bispo
Alexandra Mendes

abstract: Mobile devices have become integral to our everyday lives, yet their utility hinges on their battery life. In Android apps, resource leaks caused by inefficient resource management are a significant contributor to battery drain and poor user experience. Our work introduces Alpakka, a source-to-source compiler for Android's Smali syntax. To showcase Alpakka's capabilities, we developed an Alpakka library capable of detecting and automatically correcting resource leaks in Android APK files. We demonstrate Alpakka's effectiveness through empirical testing on 124 APK files from 31 real-world Android apps in the DroidLeaks [12] dataset. In our analysis, Alpakka identified 93 unique resource leaks, of which we estimate 15% are false positives. From these, we successfully applied automatic corrections to 45 of the detected resource leaks.


title: Handling Grammar Cycles in the 1997 SML Definition

authors:
Elizabeth Scott
Adrian Johnstone

abstract: Fully general parsers permit the syntax specification of formal languages to be unrestricted, allowing language designers to use a syntax specification that supports semantics specification, but also permitting ambiguity. Language workbenches that support fully general grammars need tools which can generate robust default behaviour but also allow experienced designers to specify particular choices when ambiguity is encountered. The standard longest match approach to ambiguity resolution is not robust when a grammar contains cycles. Although cycles can be removed from a grammar, this disrupts the syntax specification. We present an algorithm that safely removes cycles from the shared packed parse forests generated by general parsers and explore the application of the algorithm to the 1997 SML Definition. The algorithm results in a sub-forest to which further designer-specified or default disambiguation rules can be applied.


title: Can Programming Be Liberated from the Functional Style?

abstract: In his 1977 ACM Turing Award Lecture, John Backus identified the word-at-a-time style of programming, inherited from the underlying hardware and dubbed the "von Neumann bottleneck", as a major obstacle to the advancement of programming. In this keynote, I argue that the functional programming he advocated introduced its own bottleneck: that everything produced by a computation (including nothing) must be encoded as a single value. This "obligation to singularity" is foreign to modelling, where single values sit collegially between no values and two values. Exploring diverse examples, I will argue that adopting a modelling (de facto: relational) style of programming eliminates the functional bottleneck, and with it many of the data-to-control flow escapes that Backus originally sought to avoid.


title: Tool Paper: AGTix: Concise Use of Scope Graphs in Reference Attribute Grammars

abstract: This tool paper introduces AGTix, an extension to reference attribute grammars that allows constraints, inspired by Visser et al.'s Statix system, that construct and query scope graphs to be written alongside traditional attribute equations. Previous work has shown that a restricted form of Statix specifications can be translated to an equivalent reference attribute grammar that produces the same results; however, the resulting attribute grammar is quite verbose. In AGTix specifications, the more concise constraints for specifying new scope nodes or edges are translated down to the verbose equations which propagate scope node and edge information up and down the syntax tree. The query constructs for resolving names are translated down to expressions; as in Statix, these include syntax for regular expressions over edge labels that describe the valid paths for a resolution. The scope graphs and query results described by these new constructs can be used in traditional attribute grammar equations for other language processing tasks such as collecting error and warning messages or using variable types to support a translation to another language. AGTix is implemented as an extension to Silver, a full-featured extensible attribute grammar system, and is evaluated by implementing several variations of the LM language introduced by Visser et al.


title: We built the languages. That was the easy part

abstract: For over 20 years, the Software Language Engineering community has pushed languages forward. More expressive. More formal. Better tooled. Metamodeling frameworks, transformations, graphical and textual notations, language workbenches. At Obeo, we have contributed to this journey through the Eclipse ecosystem with technologies such as EMF, Acceleo, Sirius, and Capella, deployed in large-scale industrial contexts.


title: How much does an LLM know about my programming language?

authors:
David Delgado
Lola Burgueño
Robert Clarisó

abstract: Large Language Models (LLMs) are increasingly used for code generation, yet their support for programming languages is uneven, particularly for low-resource languages and infrequently used language constructs. Existing evaluation methodologies primarily assess functional correctness through test execution, which fails to reveal blind spots in a model's knowledge of a target language. In this paper, we introduce a systematic framework to identify and quantify the syntactic knowledge exhibited by an LLM with respect to a given programming language. We define syntactic coverage as a set of measurable indicators of how comprehensively language constructs are represented in datasets and generated code. Our approach analyzes code snippets against grammatical rules and structural features to compute interpretable coverage metrics, detect underrepresented constructs, and expose gaps in language support. The proposed framework supports comparative analysis across datasets, languages, and models through an automated pipeline that produces actionable diagnostic reports. Our experimental results demonstrate that syntactic coverage analysis reveals substantial differences in language support that are not captured by functional correctness alone, enabling more informed model selection, benchmark design, and dataset improvement strategies.


title: Dynamic Wind for OCaml Effect Handlers with Escaping Continuation Support

authors:
Antonino Yann William Gillard
Tetsuro Yamazaki
Tomoharu Ugawa

abstract: Effect handlers and dynamic wind provide mechanisms for implementing language constructs, such as generators and dynamically scoped variables, as libraries or embedded domain-specific languages (EDSLs). This paper presents a library implementation of dynamic wind in OCaml that is composable with effect handlers in OCaml. Their composition is challenging, especially when a delimited continuation captured by an effect handler escapes the handler's scope. Indeed, a straightforward retrofitting of Voigt's dynamic wind, originally implemented in Effekt, does not behave intuitively. In particular, it fails to implement dynamically scoped variables when a generator created within a dynamic wind scope resumes outside that scope. This is because Voigt's approach captures only the dynamic winds inside delimited continuations. Our key idea is to decorate delimited continuations with the dynamic winds enclosing the effect handler, i.e., the delimited continuation itself. We implement our dynamic wind library on top of OCaml's effect handlers and demonstrate that our design yields intuitive behavior.


title: A nanopass approach to a modular RDF implementation

authors:
Duncan Guthrie
Paul Harvey
Michele Sevegnani

abstract: Resource Description Framework (RDF) is a widespread W3C standard defining a domain-specific language for knowledge representation, providing a platform to build higher-level languages such as OWL or SHACL. RDF concrete syntaxes define an external representation of its abstract model for data interchange. Despite sharing the same core semantics, RDF concrete syntaxes differ in how well they support common modelling idioms at the surface level. Many RDF libraries have been implemented in Scheme, however, they support few concrete syntaxes and/or do not exhibit compliance with the W3C test suites.


title: Multi-Dimensional Context-Oriented Programming with a Lightweight Domain Specific Language

authors:
Christian Gutsche
Sebastian Götz
Uwe Aßmann

abstract: Context-awareness is crucial for developing cyber-physical systems to enable dynamic behavior. Context-oriented programming (COP) aims to improve the definition of context-dependent behavioral variations. However, existing layer-based COP approaches have two major limitations: layered methods are specified only for single contextual dimensions and restrict adaptations to method replacement or input/output filtering, limiting expressiveness for complex context dependencies.


title: Incremental, bidirectional text-to-text synchronizations with AnyText

abstract: Maintaining consistency across heterogeneous textual DSLs that describe the same system is a recurring challenge in software language engineering. We advocate a separation of concerns: (i) language-specific model-to-text synchronizations that relate the concrete syntax to its abstract representation as a model, and (ii) heterogeneous model-to-model synchronizations that capture the semantic overlap between languages. We extend the AnyText language workbench with a generic, grammar-based, incremental, bidirectional model-to-text synchronization by integrating its incremental parser and pretty-printer to propagate edits and support round-trip updates. Composing two such model-to-text synchronizations with an online-incremental, bidirectional model-to-model synchronization yields an end-to-end, modular, incremental, bidirectional text-to-text synchronization pipeline across DSLs. We demonstrate and evaluate the approach by synchronizing finite state machines and Petri nets, indicating a good performance of our approach also for large text documents. An open-source implementation is available under a BSD-3 license as part of NMF.


title: Engineering Verified Model Transformations through a Proof-Based Language Workbench

authors:
Akram Idani
Germán Vega

abstract: Model-driven transformations play a central role in MDE processes, yet their correctness is most often validated through testing or simulation. However, in contexts where critical scenarios may compromise system integrity or certification objectives, stronger guarantees are necessary. This paper investigates how the B method can support transformation engineering through verified formal specifications. To this end, we developed BCerT, an extension of the Meeduse language workbench, originally dedicated to the formal modeling of domain-specific languages. In our approach, transformations are defined as B operations or B events, allowing animation and model checking with ProB, as well as theorem proving with Atelier B. We discuss three complementary specification strategies: (i) a rule-oriented modeling approach optionally controlled with CSP||B; (ii) a property-driven operational B specification in which the transformation is expressed as a relation constrained by invariants; and (iii) an Event-B system capturing the transformation as atomic events focused on the end state. The approach is illustrated through two applications: the verification of a Truth Tables to Binary Decision Diagrams transformation presented at the Transformation Tool Contest, and the development of U2BCerT, a certified transpiler from UML state machines to Event-B.


title: Why Just-In-Time Compilation Matters: Evaluating Runtime and Energy Efficiency

authors:
Luís Maia
Simão Cunha
João Saraiva

abstract: Just-in-time (JIT) compilation is a core feature of many modern programming languages, combining the portability of interpreted languages with the performance benefits of ahead-of-time compilation. Originally introduced to improve the runtime performance of interpreted languages, JIT compilation dynamically compiles frequently executed code during program execution.


title: CPSLint: A Domain-Specific Language Providing Data Validation and Sanitisation for Industrial Cyber-Physical Systems

authors:
Uraz Odyurt
Ömer Sayilir
Mariëlle Stoelinga
Vadim Zaytsev

abstract: Industrial cyber-physical systems generate vast amounts of semi-structured time-series data that require careful preprocessing before they can be effectively used for machine learning applications such as fault detection and identification. Raw sensor datasets are often corrupted or incomplete, making it challenging to develop reliable solutions without proper data preparation and validation. In this paper, we introduce CPSLint, a domain-specific language for data validation and sanitisation. We present the design, implementation and evaluation of CPSLint, demonstrating its ability to automatically detect and correct common data corruption patterns while enabling non-programming domain experts to effectively prepare their data for analysis. We report evaluation results on a representative dataset, tracking memory consumption and CPU-time for sanitisation activities. Our approach offers several advantages over traditional methods, including reduced manual effort, guaranteed consistency and broader applicability across time-series datasets and projects.


title: Ztrategic: Libraries and Tools For Software Language Specification, Transformation, and Testing

authors:
Emanuel Rodrigues
José Nuno Macedo
João Saraiva

abstract: This tool paper presents the Ztrategic framework, which integrates strategic term rewriting and attributes grammars through a unifying navigation abstraction based on functional zippers. The resulting zipper-based embedding is both concise and expressive, integrating the strengths of both formalisms. Together, these mechanisms serve as foundational building blocks for Ztrategic for supporting property-based testing in language engineering.


title: A Shallow Embedding of Datalog in Lean

abstract: Datalog is a lightweight logic programming language, based on the logic of Horn clauses. Lean, on the other hand, is a proof assistant system and language based on the Calculus of Inductive Constructions (CIC). Datalog is more constrained and less expressive than Lean but has a long history of established deduction algorithms. Writing definitions and queries in the Datalog fragment of Lean would be more succinct and understandable than writing them in Lean itself.


title: Enabling Navigability of Programming Language Specifications: A Case of ECMAScript (JavaScript) Standard Library Specification

authors:
Alberto Tontoni
Mikhail Barash

abstract: Many widely adopted programming languages (e.g., C++, Java, JavaScript, WebAssembly) have specification documents that provide authoritative answers about the language and its semantics. However, such specification documents are oftentimes demanding to read and navigate. This especially manifests when a text, a PDF, or an HTML document describes the language semantics using a pseudo-code notation—which is treated as text rather than code. Readers of a language specification are thus left without any dedicated tool support to navigate the pseudo-code.


title: SLE as an Evolving Body of Knowledge: A 19-Year Comparative Analysis of Calls and Proceedings

abstract: The Software Language Engineering (SLE) community has accumulated nearly two decades of content. This content comprises not only papers as such, but also other tangible artefacts like conference descriptions, calls for papers, tools, repositories. Yet, the field's self-description (how it positions itself to potential contributors) and its accumulated output (what the community actually produces) are rarely studied together in a reproducible, fine-grained way.


venue: tacas

title: On Automatic and Interactive Design of Communication Systems

authors:
Jürgen Bohn
Stephan Rössig


title: A Front-End Generator for Verification Tools

authors:
Rance Cleaveland
Eric Madelaine
Steve Sims


title: Efficient Simplification of Bisimulation Formulas

authors:
Uffe Engberg
Kim S. Larsen


title: Model Checking of Non-Finite State Processes by Finite Approximations

authors:
Nicoletta De Francesco
Alessandro Fantechi
Stefania Gnesi
Paola Inverardi


title: Mona: Monadic Second-Order Logic in Practice

authors:
Jesper G. Henriksen
Jakob L. Jensen
Michael E. Jørgensen
Nils Klarlund
Robert Paige
Theis Rauhe
Anders Sandholm

abstract: The purpose of this article is to introduce Monadic Second-order Logic as a practical means of specifying regularity. The logic is a highly succinct alternative to the use of regular expressions. We have built a tool MONA, which acts as a decision procedure and as a translator to finite-state automata. The tool is based on new algorithms for minimizing finite-state automata that use binary decision diagrams (BDDs) to represent transition functions in compressed form. A byproduct of this work is an algorithm that matches the time but improves the space of Sieling and Wegener's algorithm to reduce OBDDs in linear time.


title: A User Guide to HyTech

authors:
Thomas A. Henzinger
Pei-Hsin Ho
Howard Wong-Toi


title: Layers as Knowledge Transitions in the Design of Distributed Systems


title: Parallelism for Free: Bitvector Analyses -> No State Explosion!

authors:
Jens Knoop
Bernhard Steffen
Jürgen Vollmer


title: A Constraint Oriented Proof Methodology Based on Modal Transition Systems

authors:
Kim Guldstrand Larsen
Bernhard Steffen
Carsten Weise

abstract: We present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which can be refined by successively adding constraints. Key concepts of our method are projective views, separation of proof obligations, Skolemization and abstraction. Central to the method is the use of Parametrized Modal Transition Systems. The method easily transfers to real-time systems, where the main problem are parameters in timing constraints.


title: Modal µ-Calculus, Model Checking and Gauß Elimination


title: Combining Model Checking and Deduction for I/O-Automata

authors:
Olaf Müller
Tobias Nipkow


title: Hierarchical Compression for Model-Checking CSP or How to Check 1020 Dining Philosophers for Deadlock

authors:
A. W. Roscoe
Paul H. B. Gardiner
Michael Goldsmith
J. R. Hulance
D. M. Jackson
J. Bryan Scattergood


title: Analytic and Locally Approximate Solutions to Properties of Probabilistic Processes


title: An Analyser for Mesage Sequence Charts

authors:
Rajeev Alur
Gerard J. Holzmann
Doron A. Peled


title: Generic System Support for Deductive Program Development

authors:
Abdelwaheb Ayari
David A. Basin


title: UPPAAL in 1995

authors:
Johan Bengtsson
Kim Guldstrand Larsen
Fredrik Larsson
Paul Pettersson
Wang Yi

abstract: Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata [12, 9, 4], developed during the past two years. In this paper, we summarize the main features of Uppaal in particular its various extensions developed in 1995 as well as applications to various case-studies, review and provide pointers to the theoretical foundation.


title: Realtion-Algebraic Analysis of Petri Nets with RELVIEW

authors:
Rudolf Berghammer
Burghard von Karger
Christiane Ulke


title: Efficent Local Model-Checking for Fragments of teh Modal µ-Calculus

authors:
Girish Bhat
Rance Cleaveland


title: The FC2TOOLS Set (Tool Demonstration)

authors:
Amar Bouali
Annie Ressouche
Valérie Roy
Robert de Simone


title: Strategy Construction in Infinite Ganes with Streett and Rabin Chain Winning Conditions

authors:
Nils Buhrke
Helmut Lescow
Jens Vöge


title: Formal Verification of a Partial-Order Reduction Technique for Model Checking

authors:
Ching-Tsun Chou
Doron A. Peled


title: Priorities for Modeling and Verifying Distributed Systems

authors:
Rance Cleaveland
Gerald Lüttgen
V. Natarajan
Steve Sims


title: The Concurrency Factory Software Development Environment

authors:
Rance Cleaveland
Philip M. Lewis
Scott A. Smolka
Oleg Sokolsky


title: Rapid Prototyping for an Assertional Specification language

authors:
Jorge Cuéllar
Dieter Barnard
Martin Huber


title: Efficient Search as a Means of Executing Specifications

authors:
Craig Damon
Daniel Jackson


title: An Improvement of McMillan's Unfolding Algorithm

authors:
Javier Esparza
Stefan Römer
Walter Vogler


title: Automatic Compositional Verification of Some Security Properties

authors:
Riccardo Focardi
Roberto Gorrieri


title: PEP - More than a Petri Net Tool

authors:
Bernd Grahlmann
Eike Best


title: A Construction and Analysis Tool Based on the Stochastic Process Algebra TIPP

authors:
Holger Hermanns
Vassilis Mertsiotakis
Michael Rettelbach


title: cTc - A Tool Supporting the Construction of cTLA-Specifications

authors:
Carsten Heyl
Arnulf Mester
Heiko Krumm


title: Early Fault Detection Tools


title: DFA&OPT-METAFrame: A Tool Kit for Program Analysis and Optimazation

authors:
Marion Klein
Jens Knoop
Dirk Koschützki
Bernhard Steffen


title: Timed Condition/Event Systems: A Framework for Modular Discrete Models of Chemical Plants and Verification of Their Real-Time Discrete Control

authors:
Stefan Kowalewski
Jörg Preußig


title: Kleene Algebra with Tests and Commutativity Conditions


title: Managing Proofs (Abstract)


title: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR


title: Fully Automatic Verifcation and Error Detection for Parameterized Iterative Sequential Circuits


title: Permutable Agents in Process Algebras

authors:
François Michel
Pierre Azéma
François Vernadat


title: Probabilistic Duration Automata for Analyzing Real-Time Systems

authors:
Louise E. Moser
P. M. Melliar-Smith


title: Reactive EFSMs - Reactive Promela/RSPIN

authors:
Elie Najm
Frank Olsen


title: Using the Constraint Language Toupie for "Software Cost Reduction" Specification Analysis (Abstract)


title: A Tool for Proving Invariance Properties of Concurrent Systems Automatically


title: A Constraint-Oriented Service Creation Environment

authors:
Bernhard Steffen
Tiziana Margaria
Andreas Claßen
Volker Braun
Rita Nisius
Manfred Reitenspieß


title: Games and Modal Mu-Calculus


title: Test Generation with Inputs, Outputs, and Quiescence


title: Extending Promela and Spin for Real Time

authors:
Stavros Tripakis
Costas Courcoubetis


title: Visual Verification of Reactive Systems

authors:
Luca de Alfaro
Zohar Manna
Henny B. Sipma
Tomás E. Uribe


title: Partial Model Checking with ROBDDs

authors:
Henrik Reif Andersen
Jørgen Staunstrup
Niels Maretti


title: Graphs in METAFrame: The Unifying Power of Polymorphism

authors:
Michael von der Beeck
Volker Braun
Andreas Claßen
Achim Dannecker
Carsten Friedrich
Dirk Koschützki
Tiziana Margaria
Falk Schreiber
Bernhard Steffen


title: Syntactic Detection of Process Divergence and Non-local Choice inMessage Sequence Charts

authors:
Hanêne Ben-Abdallah
Stefan Leue

abstract: Message Sequence Charts (MSCs) are increasingly used in software engineering methodologies and tools to capture, for instance, system requirements, test scenarios, and simulation traces. They have been standardized by ITU-T in Recommendation Z.120 [IT96]. However, various aspects of environment behavior remain underspecified in MSCs, e.g., the presence of resources for inter-process communication and the coordination of concurrent processes at points of control branching. Such underspecifications can result in ambiguities in an MSC specification and discrepancies between an MSC specification and its implementation. In this paper we characterize two consequences of harmful underspecifications: process divergence and non-local branching choice. We also present two syntax-based analysis algorithms that detect both problems.


title: Hardware and Software Synthesis, Optimization, and Verification from Esterel Programs


title: Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs

authors:
Bernard Boigelot
Patrice Godefroid


title: A Tool to Support Formal Reasoning about Computer Languages


title: Design/CPN - A Computer Tool for Coloured Petri Nets

authors:
Søren Christensen
Jens Bæk Jørgensen
Lars Michael Kristensen

abstract: In this paper, we describe the computer tool Design/CPN supporting editing, simulation, and state space analysis of Coloured Petri Nets. So far, approximately 40 man-years have been invested in the development of Design/CPN. It is used world-wide by more than 200 companies and research institutions. For the presentation, we draw from the experiences gained in a recent industrial application using Coloured Petri Nets in the design, validation, and verification of communication protocols for audio/video systems.


title: The Bounded Retransmission Protocol Must Be on Time!

authors:
Pedro R. D'Argenio
Joost-Pieter Katoen
Theo C. Ruys
Jan Tretmans


title: Manipulation Algorithms for K*BMDs

authors:
Rolf Drechsler
Bernd Becker
Stefan Ruppertz


title: The Term Processor Generator Kimwitu

authors:
Peter van Eijk
Axel Belinfante
Henk Eertink
Henk Alblas


title: Combining Partial Order and Symmetry Reductions

authors:
E. Allen Emerson
Somesh Jha
Doron A. Peled


title: Test Generation for Intelligent Networks Using Model Checking

authors:
André Engels
Loe M. G. Feijs
Sjouke Mauw


title: An Automated Based Verification Environment for Mobile Processes

authors:
Gian-Luigi Ferrari
Gianluigi Ferro
Stefania Gnesi
Ugo Montanari
Marco Pistore
Gioia Ristori


title: The Reference Component of PEP


title: A Brief Introduction to Coloured Petri Nets


title: MOSEL: A FLexible Toolset for Monadic Second-Order Logic

authors:
Peter Kelb
Tiziana Margaria
Michael Mendler
Claudia Gsottberger


title: Incremental Development of Deadlock-Free Communicating Systems


title: Compositional State Space Generation from Lotos Programs

authors:
Jean-Pierre Krimm
Laurent Mounier


title: Integration in PVS: Tables, Types, and Model Checking

authors:
Sam Owre
John M. Rushby
Natarajan Shankar


title: Space Efficient Reachability Analysis Through Use of Pseudo-Root States

authors:
Atanas N. Parashkevov
Jay Yantchev


title: Model-Checking for a Subclass of Event Structures


title: Formal Verification of Statecharts with Instantaneous Chain Reaction

authors:
Jan Philipps
Peter Scholz


title: Mechanically Verified Self-Stabilizing Hierarchical Algorithms


title: Real-Time Logics: Fictitious Clock as an Abstraction of Dense Time

authors:
Jean-François Raskin
Pierre-Yves Schobbens


title: Theorem Prover Support for the Refinement of Stream Processing Functions

authors:
Robert Sandner
Olaf Müller


title: A Tableau System for Linear-TIME Temporal Logic

authors:
Peter H. Schmitt
Jean Goubault-Larrecq


title: Compositional Performance Analysis


title: Verifying Networks of Timed Processes (Extended Abstract)

authors:
Parosh Aziz Abdulla
Bengt Jonsson


title: Model Checking via Reachability Testing for Timed Automata

authors:
Luca Aceto
Augusto Burgueño
Kim Guldstrand Larsen

abstract: In this paper we develop an approach to model-checking for timed automata via reachability testing. As our specification formalism, we consider a dense-time logic with clocks. This logic may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every logical formula phi, a so-called test automaton T_phi in such a way that checking whether a system S satisfies the property phi can be reduced to a reachability question over the system obtained by making T_phi interact with S. The testable logic we consider is both of practical and theoretical interest. On the practical side, we have used the logic, and the associated approach to model-checking via reachability testing it supports, in the specification and verification in Uppaal of a collision avoidance protocol. On the theoretical side, we show that the logic is powerful enough to permit the definition of characteristic properties, with respect to a timed version ofthe ready simulation preorder, for nodes of deterministic, tau-free timed automata. This allows one to compute behavioural relations via our model-checking technique, therefore effectively reducing the problem of checking the existence of a behavioural relation among states of a timed automaton to a reachability problem.


title: Detecting Races in Relay Ladder Logic Programs

authors:
Alexander Aiken
Manuel Fähndrich
Zhendong Su


title: Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond

authors:
Khalil Ajami
Serge Haddad
Jean-Michel Ilié


title: Symbolic Exploration of transition Hierarchies

authors:
Rajeev Alur
Thomas A. Henzinger
Sriram K. Rajamani


title: MESA: Support for Scenario-Based Design of Concurrent Systems

authors:
Hanêne Ben-Abdallah
Stefan Leue


title: Deciding Fixed and Non-fixed Size Bit-vectors

authors:
Nikolaj S. Bjørner
Mark C. Pichora


title: Tamagotchis Need Not Die - Verification of STATEMENT Design

authors:
Udo Brockmeyer
Gunnar Wittich


title: Formal Verification of Pipelined Processors


title: Modeling and Verification of SC++ Applications


title: Set-Based Analysis of Reactive Infinite-State Systems

authors:
Witold Charatonik
Andreas Podelski


title: Model Checking of Real-Time Reachability Properties Using Abstractions

authors:
Conrado Daws
Stavros Tripakis


title: OPEN/CÆSAR: An OPen Software Architecture for Verification, Simulation, and Testing


title: Combining Finite Automata, Parallel Programs and SDL Using Petri Nets


title: Automated Verification of Szymanski's Algorithm

authors:
E. Pascal Gribomont
Guy Zenner


title: Verification Based on Local States

authors:
Michaela Huhn
Peter Niebert
Frank Wallner


title: A Proof of Burns N-Process Mutual Exclusion Algorithm Using Abstraction

authors:
Henrik Ejersbo Jensen
Nancy A. Lynch


title: Static Partial Order Reduction

authors:
Robert P. Kurshan
Vladimir Levin
Marius Minea
Doron A. Peled
Hüsnü Yenigün


title: Modular Model Checking of Software

authors:
Karen Laster
Orna Grumberg


title: Verification of Large State/Event Systems Using Compositionality and Dependency Analysis

authors:
Jørn Lind-Nielsen
Henrik Reif Andersen
Gerd Behrmann
Henrik Hulgaard
Kåre J. Kristoffersen
Kim Guldstrand Larsen


title: Formal Design and Analysis of a Gear Controller

authors:
Magnus Lindahl
Paul Pettersson
Wang Yi


title: Fully Local and Efficient Evaluation of Alternating Fixed Points (Extended Abstract)

authors:
Xinxin Liu
C. R. Ramakrishnan
Scott A. Smolka


title: Translation Validation

authors:
Amir Pnueli
Michael Siegel
Eli Singerman


title: Formal Verification of SDL Systems at the Siemens Mobile Phone Department

authors:
Franz Regensburger
Aenne Barnard


title: Experience with Literate Programming in the Modelling and Validation of Systems

authors:
Theo C. Ruys
Ed Brinksma


title: Factotum: Automatic and Systematic Sharing Support for Systems Analyzers

authors:
David James Sherman
Nicolas Magnier


title: A Verified Model Checker for the Modal µ-calculus in Coq


title: Practical Model-Checking Using Games

authors:
Perdita Stevens
Colin Stirling


title: Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation

authors:
Miroslav N. Velev
Randal E. Bryant


title: Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol

authors:
Parosh Aziz Abdulla
Aurore Annichini
Ahmed Bouajjani


title: DYANA: An Environment for Embedded System Design and Analysis

authors:
Anatoly G. Bakhmurov
A. P. Kapitonova
Ruslan L. Smeliansky


title: Process Algebra in PVS

authors:
Twan Basten
Jozef Hooman


title: Verification of Hierarchical State/Event Systems Using Reusability and Compositionality

authors:
Gerd Behrmann
Kim Guldstrand Larsen
Henrik Reif Andersen
Henrik Hulgaard
Jørn Lind-Nielsen


title: An Automated Analysis of Ping-Pong Interactions in E-mail Services

authors:
Anne Bergeron
Jean-Christophe Manzoni


title: Symbolic Model Checking without BDDs

authors:
Armin Biere
Alessandro Cimatti
Edmund M. Clarke
Yunshan Zhu

abstract: Symbolic Model Checking [3, 14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stalmarck's Method [16] or the Davis & Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability. We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented.


title: The ETI Online Service in Action

authors:
Volker Braun
Jürgen Kreileder
Tiziana Margaria
Bernhard Steffen


title: Modular State Level Analysis of Distributed Systems Techniques and Tool Support

authors:
Peter Buchholz
Peter Kemper


title: Model Checking in CLP

authors:
Giorgio Delzanno
Andreas Podelski


title: Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools

authors:
Yifei Dong
Xiaoqun Du
Y. S. Ramakrishna
C. R. Ramakrishnan
I. V. Ramakrishnan
Scott A. Smolka
Oleg Sokolsky
Eugene W. Stark
David Scott Warren


title: Analyzing Stochastic Fixed-Priority Real-Time Systems

authors:
Mark K. Gardner
Jane W.-S. Liu


title: Path Exploration Tool

authors:
Elsa L. Gunter
Doron A. Peled


title: Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets


title: Specifications and Proofs for Ensemble Layers

authors:
Jason Hickey
Nancy A. Lynch
Robbert van Renesse


title: On the Benefits of Using the Up-To Techniques for Bisimulation Verification


title: Scheduling System Verification

authors:
Pao-Ann Hsiung
Farn Wang
Yue-Sun Kuo


title: Hardware Testing Using a Communication Protocol Conformance Testing Tool

authors:
Hakim Kahlouche
César Viho
Massimo Zendri


title: A Light-Weight Framework for Hardware Verification

authors:
Christoph Kern
Tarik Ono-Tesfaye
Mark R. Greenstreet


title: From DFA-Frameworks to DFA-Generators: A Unifying Multiparadigm Approach


title: Modelling for Mere Mortals

authors:
Jeff Kramer
Jeff Magee


title: Automated Fast-Track Reconfiguration of Group Communication Systems


title: Computing Strong/Weak Bisimulation Equivalences and Observation Congruence for Value-Passing Processes

authors:
Zhoujun Li
Huowang Chen


title: Automatic Verification of Cryptographic Protocols through Compositional Analysis Techniques

authors:
Davide Marchignoli
Fabio Martinelli


title: Finite State Verification for the Asynchronous pi-Calculus

authors:
Ugo Montanari
Marco Pistore


title: An Easily Extensible Toolset for Tabular Mathematical Expressions

authors:
David Lorge Parnas
Dennis K. Peters


title: Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL


title: On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction

authors:
Vlad Rusu
Eli Singerman


title: A Period Assignment Algorithm for Real-Time System Design

authors:
Minsoo Ryu
Seongsoo Hong


title: A Theorem Prover-Based Analysis Tool for Object-Oriented Databases

authors:
David Spelt
Susan J. Even


title: Some Issues in the Software Engineering of Verification Tools


title: Timed Diagnostics for Reachability Properties


title: Symbolic Reachability Analysis Based on SAT-Solvers

authors:
Parosh Aziz Abdulla
Per Bjesse
Niklas Eén


title: Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation

authors:
Luca de Alfaro
Marta Z. Kwiatkowska
Gethin Norman
David Parker
Roberto Segala


title: A Comparison of Two Verification Methods for Speculative Instruction Execution

authors:
Tamarah Arons
Amir Pnueli


title: Proof General: A Generic Tool for Proof Development


title: Abstracting WS1S Systems to Verify Parameterized Networks

authors:
Kai Baukus
Saddek Bensalem
Yassine Lakhnech
Karsten Stahl


title: Model Checking Security Protocols Using a Logic of Belief

authors:
Massimo Benerecetti
Fausto Giunchiglia


title: Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking

authors:
Ramesh Bharadwaj
Steve Sims


title: FMona: A Tool for Expressing Validation Techniques over Infinite State Systems

authors:
Jean-Paul Bodeveix
Mamoun Filali


title: On the Construction of Live Timed Systems

authors:
Sébastien Bornot
Gregor Gößler
Joseph Sifakis


title: Model Checking SDL with Spin

authors:
Dragan Bosnacki
Dennis Dams
Leszek Holenderski
Natalia Sidorova


title: Using Static Analysis to Improve Automatic Test Generation

authors:
Marius Bozga
Jean-Claude Fernandez
Lucian Ghirvu


title: Consistent Integration of Formal Methods

authors:
Peter Braun
Heiko Lötzbeyer
Bernhard Schätz
Oscar Slotosch


title: BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems


title: Model Checking Support for the ASM High-Level Language

authors:
Giuseppe Del Castillo
Kirsten Winter


title: Partial Order Reductions for Security Protocol Verification

authors:
Edmund M. Clarke
Somesh Jha
Wilfredo R. Marrero

abstract: In this paper we explore partial order reduction that make the task of verifying cryptographic protocols more efficient. These reduction techniques have been implemented in our tool BRUTUS. A lthough we have implemented several reduction techniques in our tool BRUTUS, due to space restrictions in this paper we only focus on partial order reductions. Partial order reductions have proved very useful in the domain of model checking reactive systems. These reductions are not directly applicable in our context because of additional complications caused by tracking knowledge of various agents. We present partial order reductions in the context of verifying security protocols and prove their correctness. Experimental results showing the benefits of this reduction technique are also presented.


title: Symbolic Representation of Upward-Closed Sets

authors:
Giorgio Delzanno
Jean-François Raskin


title: The PROSPER Toolkit

authors:
Louise A. Dennis
Graham Collins
Michael Norrish
Richard J. Boulton
Konrad Slind
Graham Robinson
Michael J. C. Gordon
Thomas F. Melham


title: A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors

authors:
Stefania Gnesi
Diego Latella
Gabriele Lenzini
C. Abbaneo
Arturo M. Amendola
P. Marmo


title: ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation

authors:
Michael Goedicke
Bettina Enders
Torsten Meyer
Gabriele Taentzer


title: Checking for CFFD-Preorder with Tester Processes

authors:
Juhana Helovuo
Antti Valmari


title: Symbolic Model Checking for Rectangular Hybrid Systems

authors:
Thomas A. Henzinger
Rupak Majumdar


title: Fair Bisimulation

authors:
Thomas A. Henzinger
Sriram K. Rajamani


title: A Markov Chain Model Checker

authors:
Holger Hermanns
Joost-Pieter Katoen
Joachim Meyer-Kayser
Markus Siegle


title: Transitive Closures of Regular Relations for Verifying Infinite-State Systems

authors:
Bengt Jonsson
Marcus Nilsson


title: VIP: A Visual Editor and Compiler for v-Promela

authors:
Moataz Kamel
Stefan Leue


title: Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems

authors:
Jean-Pierre Krimm
Laurent Mounier


title: On Memory-Block Traversal Problems in Model-Checking Timed-Systems

authors:
Fredrik Larsson
Paul Pettersson
Wang Yi

abstract: A major problem in model-checking timed systems is the huge memory requirement. In this paper, we study the memory-block traversal problems of using standard operating systems in exploring the state-space of timed automata. We report a case study which demonstrates that deallocating memory blocks (i.e. memory-block traversal) using standard memory management routines is extremely time-consuming. The phenomenon is demonstrated in a number of experiments by installing the UPPAAL tool on Windows95, SunOS 5 and Linux. It seems that the problem should be solved by implementing a memory manager for the model-checker, which is a troublesome task as it is involved in the underlining hardware and operating system. We present an alternative technique that allows the model-checker to control the memory-block traversal strategies of the operating systems without implementing an independent memory manager. The technique is implemented in the UPPAAL model-checker. Our experiments demonstrate that it results in significant improvement on the performance of UPPAAL. For example, it reduces the memory deallocation time in checking a start-up synchronisation protocol on Linux from 7 days to about 1 hour. We show that the technique can also be applied in speeding up re-traversals of explored state-space.


title: Efficient Diagnostic Generation for Boolean Equation Systems


title: An Architecture for Interactive Program Provers

authors:
Jörg Meyer
Arnd Poetzsch-Heffter


title: CASL: From Semantics to Tools


title: Tool-Based Specification of Visual Languages and Graphic Editors

authors:
Magnus Niemann
Roswitha Bardohl


title: Verification of Parameterized Systems Using Logic Program Transformations

authors:
Abhik Roychoudhury
K. Narayan Kumar
C. R. Ramakrishnan
I. V. Ramakrishnan
Scott A. Smolka


title: Integrating Low Level Symmetries into Reachability Analysis


title: Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems


title: On the Construction of Automata from Linear Arithmetic Constraints

authors:
Pierre Wolper
Bernard Boigelot


title: An Extensible Type System for Component-Based Design

authors:
Yuhong Xiong
Edward A. Lee


title: Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams

authors:
Nina Amla
E. Allen Emerson
Kedar S. Namjoshi
Richard J. Trefler


title: Abstraction in Probabilistic Process Algebra

authors:
Suzana Andova
Jos C. M. Baeten


title: Parameterized Verification of Multithreaded Software Libraries

authors:
Thomas Ball
Sagar Chaki
Sriram K. Rajamani


title: Boolean and Cartesian Abstraction for Model Checking C Programs

authors:
Thomas Ball
Andreas Podelski
Sriram K. Rajamani


title: CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS

authors:
Michel Beaudouin-Lafon
Wendy E. Mackay
Mads Jensen
Peter Andersen
Paul Janecek
Henry Michael Lassen
Kasper Lund
Kjeld Høyer Mortensen
Stephanie Munck
Anne V. Ratzer
Katrine Ravn
Søren Christensen
Kurt Jensen


title: Efficient Guiding Towards Cost-Optimality in UPPAAL

authors:
Gerd Behrmann
Ansgar Fehnker
Thomas Hune
Kim G. Larsen
Paul Pettersson
Judi Romijn

abstract: In this paper we present an algorithm for efficiently computing the minimum cost of reaching a goal state in the model of Uniformly Priced Timed Automata (UPTA). This model can be seen as a submodel of the recently suggested model of linearly priced timed automata, which extends timed automata with prices on both locations and transitions. The presented algorithm is based on a symbolic semantics of UTPA, and an efficient representation and operations based on difference bound matrices. In analogy with Dijkstra's shortest path algorithm, we show that the search order of the algorithm can be chosen such that the number of symbolic states explored by the algorithm is optimal, in the sense that the number of explored states can not be reduced by any other search order. We also present a number of techniques inspired by branch-and-bound algorithms which can be used for limiting the search space and for quickly finding near-optimal solutions.The algorithm has been implemented in the verification tool UPPAAL. When applied on a number of experiments the presented techniques reduced the explored state-space with up to 90%.


title: The LOOP Compiler for Java and JML

authors:
Joachim van den Berg
Bart Jacobs


title: Parallel Model Checking for the Alternation Free µ-Calculus

authors:
Benedikt Bollig
Martin Leucker
Michael Weber


title: Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets

authors:
Rubén Carvajal-Schiaffino
Giorgio Delzanno
Giovanni Chiola


title: The ASM Workbench - A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models Tool Demonstration


title: Implementing a Multi-valued Symbolic Model Checker

authors:
Marsha Chechik
Benet Devereux
Steve M. Easterbrook


title: Coverage Metrics for Temporal Logic Model Checking

authors:
Hana Chockler
Orna Kupferman
Moshe Y. Vardi


title: A Sweep-Line Method for State Space Exploration

authors:
Søren Christensen
Lars Michael Kristensen
Thomas Mailund


title: Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation

authors:
Gianfranco Ciardo
Gerald Lüttgen
Radu Siminiceanu


title: Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking

authors:
Alessandro Cimatti
Marco Roveri
Piergiorgio Bertoli


title: Synthesis of Linear Ranking Functions

authors:
Michael Colón
Henny Sipma


title: Language Containment Checking with Nondeterministic BDDs


title: Is There a Best Symbolic Cycle-Detection Algorithm?

authors:
Kathi Fisler
Ranan Fraer
Gila Kamhi
Moshe Y. Vardi
Zijiang Yang


title: Propositional Reasoning


title: Verification of Vortex Workflows

authors:
Xiang Fu
Tevfik Bultan
Richard Hull
Jianwen Su


title: Compositional Message Sequence Charts

authors:
Elsa L. Gunter
Anca Muscholl
Doron A. Peled


title: Linear Parametric Model Checking of Timed Automata

authors:
Thomas Hune
Judi Romijn
Mariëlle Stoelinga
Frits W. Vaandrager


title: Testing an Intentional Naming Scheme Using Genetic Algorithms


title: An Automata Based Interpretation of Live Sequence Charts

authors:
Jochen Klose
Hartmut Wittke


title: Incremental Verification by Abstraction

authors:
Yassine Lakhnech
Saddek Bensalem
Sergey Berezin
Sam Owre


title: Hardware/Software Co-Design Using Functional Languages

authors:
Alan Mycroft
Richard Sharp


title: Automated Test Generation from Timed Automata

authors:
Brian Nielsen
Arne Skou


title: The Erlang Verification Tool

authors:
Thomas Noll
Lars-Åke Fredlund
Dilian Gurov


title: Model Checking CTL*[DC]


title: Finding Feasible Counter-examples when Model Checking Abstracted Java Programs

authors:
Corina S. Pasareanu
Matthew B. Dwyer
Willem Visser


title: Automatic Deductive Verification with Invisible Invariants

authors:
Amir Pnueli
Sitvanit Ruah
Lenore D. Zuck


title: Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions

authors:
Filippo Ricca
Paolo Tonella


title: First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders

authors:
Theo C. Ruys
Rom Langerak
Joost-Pieter Katoen
Diego Latella
Mieke Massink


title: Model Checking Syllabi and Student Carreers

authors:
Roberto Sebastiani
Alessandro Tomasi
Fausto Giunchiglia


title: TATOO: Testing and Analysis Tool for Object- Oriented Software

authors:
Amie L. Souter
Tiffany M. Wong
Stacey A. Shindo
Lori L. Pollock


title: Simulation Revisited

authors:
Li Tan
Rance Cleaveland


title: A Technique for Invariant Generation

authors:
Ashish Tiwari
Harald Rueß
Hassen Saïdi
Natarajan Shankar


title: Branching vs. Linear Time: Final Showdown


title: Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors


title: Satisfiability Checking Using Boolean Expression Diagrams

authors:
Poul Frederick Williams
Henrik Reif Andersen
Henrik Hulgaard


title: A Library for Composite Symbolic Representations

authors:
Tuba Yavuz-Kahveci
Murat Tuncer
Tevfik Bultan


title: Preemptive Job-Shop Scheduling Using Stopwatch Automata

authors:
Yasmina Abdeddaïm
Oded Maler


title: TIMES - A Tool for Modelling and Implementation of Embedded Systems

authors:
Tobias Amnell
Elena Fersman
Leonid Mokrushin
Paul Pettersson
Wang Yi


title: The ForSpec Temporal Logic: A New Temporal Property-Specification Language

authors:
Roy Armoni
Limor Fix
Alon Flaisher
Rob Gerth
Boris Ginsburg
Tomer Kanza
Avner Landver
Sela Mador-Haim
Eli Singerman
Andreas Tiemeyer
Moshe Y. Vardi
Yael Zbar


title: A Functional Semantics of Attribute Grammars


title: Relative Completeness of Abstraction Refinement for Software Model Checking

authors:
Thomas Ball
Andreas Podelski
Sriram K. Rajamani


title: Resource-Constrained Model Checking of Recursive Programs

authors:
Samik Basu
K. Narayan Kumar
L. Robert Pokorny
C. R. Ramakrishnan


title: Black Box Unfolding with Local First Search

authors:
Sébastien Bornot
Rémi Morin
Peter Niebert
Sarah Zennou


title: CLPS-B - A Constraint Solver for B

authors:
Fabrice Bouquet
Bruno Legeard
Fabien Peureux


title: Beyond Parameterized Verification

authors:
Marco Bozzano
Giorgio Delzanno


title: Improving the Verification of Timed Systems Using Influence Information

authors:
Víctor A. Braberman
Diego Garbervetsky
Alfredo Olivero


title: Applicability of Fair Simulation

authors:
Doron Bustan
Orna Grumberg


title: Validating Timing Constraints of Dependent Jobs with Variable Execution Times in Distributed Real-Time Systems

authors:
Hojung Cha
Rhan Ha


title: STG: A Symbolic Test Generation Tool

authors:
Duncan Clarke
Thierry Jéron
Vlad Rusu
Elena Zinovieva


title: Towards the Automated Verification of Multithreaded Java Programs

authors:
Giorgio Delzanno
Jean-François Raskin
Laurent Van Begin


title: Model Checking Large-Scale and Parameterized Resource Allocation Systems

authors:
E. Allen Emerson
Vineet Kahlon


title: Timed Automata with Asynchronous Processes: Schedulability and Decidability

authors:
Elena Fersman
Paul Pettersson
Wang Yi


title: Simulation as Coarsest Partition Problem

authors:
Raffaella Gentilini
Carla Piazza
Alberto Policriti


title: Exploring Very Large State Spaces Using Genetic Algorithms

authors:
Patrice Godefroid
Sarfraz Khurshid


title: Adaptive Model Checking

authors:
Alex Groce
Doron A. Peled
Mihalis Yannakakis


title: Temporal Debugging for Concurrent Systems

authors:
Elsa L. Gunter
Doron A. Peled


title: Synthesizing Monitors for Safety Properties

authors:
Klaus Havelund
Grigore Rosu


title: Parallelisation of the Petri Net Unfolding Algorithm

authors:
Keijo Heljanko
Victor Khomenko
Maciej Koutny


title: A Temporal Logic Based Theory of Test Coverage and Generation

authors:
Hyoung Seok Hong
Insup Lee
Oleg Sokolsky
Hasan Ural


title: Alloy: A New Technology for Software Modelling


title: Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis

authors:
HoonSang Jin
Andreas Kuehlmann
Fabio Somenzi


title: Fate and Free Will in Error Traces

authors:
HoonSang Jin
Kavita Ravi
Fabio Somenzi


title: Formal Verification of Functional Properties of an SCR-Style Software Requirements Specification Using PVS

authors:
Taeho Kim
David W. J. Stringer-Calvert
Sung Deok Cha


title: Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach

authors:
Marta Z. Kwiatkowska
Gethin Norman
David Parker


title: Compositional Verification Using SVL Scripts


title: Software Construction and Analysis Tools for Future Space Missions


title: Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems


title: Digitisation and Full Abstraction for Dense-Time Model Checking


title: Real-Time Systems Design with PEP


title: An Analysis of Zero-Clairvoyant Scheduling


title: Explicit Modeling of Influences, and of Their Absence, in Distributed Systems

authors:
Horst F. Wedde
Arnim Wedig


title: On Optimal Scheduling under Uncertainty

authors:
Yasmina Abdeddaïm
Eugene Asarin
Oded Maler


title: Counter-Example Guided Predicate Abstraction of Hybrid Systems

authors:
Rajeev Alur
Thao Dang
Franjo Ivancic


title: Modular Strategies for Recursive Game Graphs

authors:
Rajeev Alur
Salvatore La Torre
P. Madhusudan


title: Experimental Analysis of Different Techniques for Bounded Model Checking

authors:
Nina Amla
Robert P. Kurshan
Kenneth L. McMillan
Ricardo H. Medel


title: Resets vs. Aborts in Linear Temporal Logic

authors:
Roy Armoni
Doron Bustan
Orna Kupferman
Moshe Y. Vardi


title: A New Knowledge Representation Strategy for Cryptographic Protocol Analysis

authors:
Ivan Cibrario Bertolotti
Luca Durante
Riccardo Sisto
Adriano Valenzano


title: Code-Based Test Generation for Validation of Functional Processor Descriptions

authors:
Fabrice Baray
Philippe Codognet
Daniel Diaz
Henri Michel


title: Construction of Efficient BDDs for Bounded Arithmetic Constraints

authors:
Constantinos Bartzis
Tevfik Bultan


title: Compositional Analysis for Verification of Parameterized Systems

authors:
Samik Basu
C. R. Ramakrishnan


title: Static Guard Analysis in Timed Automata Verification

authors:
Gerd Behrmann
Patricia Bouyer
Emmanuel Fleury
Kim Guldstrand Larsen


title: Bounded Model Checking for Past LTL

authors:
Marco Benedetti
Alessandro Cimatti


title: An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic

authors:
Sergey Berezin
Vijay Ganesh
David L. Dill


title: State Class Constructions for Branching Analysis of Time Petri Nets

authors:
Bernard Berthomieu
François Vernadat


title: Automatic Test Generation with AGATHA

authors:
Céline Bigot
Alain Faivre
Jean-Pierre Gallois
Arnault Lapitre
David Lugato
Jean-Yves Pierron
Nicolas Rapin


title: Pattern-Based Abstraction for Verifying Secrecy in Protocols

authors:
Liana Bozga
Yassine Lakhnech
Michaël Périn


title: BANANA - A Tool for Boundary Ambients Nesting ANAlysis

authors:
Chiara Braghin
Agostino Cortesi
Stefano Filippone
Riccardo Focardi
Flaminia L. Luccio
Carla Piazza


title: Verification and Improvement of the Sliding Window Protocol

authors:
Dmitri Chkliaev
Jozef Hooman
Erik P. de Vink


title: Saturation Unbound

authors:
Gianfranco Ciardo
Robert M. Marmorstein
Radu Siminiceanu


title: Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement

authors:
Edmund M. Clarke
Ansgar Fehnker
Zhi Han
Bruce H. Krogh
Olaf Stursberg
Michael Theobald


title: Learning Assumptions for Compositional Verification

authors:
Jamieson M. Cobleigh
Dimitra Giannakopoulou
Corina S. Pasareanu


title: Strategies for Combining Decision Procedures

authors:
Sylvain Conchon
Sava Krstic


title: Verics: A Tool for Verifying Timed Automata and Estelle Specifications

authors:
Piotr Dembinski
Agata Janowska
Pawel Janowski
Wojciech Penczek
Agata Pólrola
Maciej Szreter
Bozena Wozna
Andrzej Zbrzezny


title: Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols

authors:
E. Allen Emerson
Vineet Kahlon


title: Simple Representative Instantiations for Multicast Protocols

authors:
Javier Esparza
Monika Maidl


title: Schedulability Analysis Using Two Clocks

authors:
Elena Fersman
Leonid Mokrushin
Paul Pettersson
Wang Yi


title: Decidability of Invariant Validation for Paramaterized Systems

authors:
Pascal Fontaine
E. Pascal Gribomont


title: Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation

authors:
Marcelo Glusman
Gila Kamhi
Sela Mador-Haim
Ranan Fraer
Moshe Y. Vardi


title: Large State Space Visualization

authors:
Jan Friso Groote
Frank van Ham


title: Proof-Like Counter-Examples

authors:
Arie Gurfinkel
Marsha Chechik


title: On the Universal and Existential Fragments of the µ-Calculus

authors:
Thomas A. Henzinger
Orna Kupferman
Rupak Majumdar


title: A Set of Performance and Dependability Analysis Components for CADP

authors:
Holger Hermanns
Christophe Joubert


title: Branching Processes of High-Level Petri Nets

authors:
Victor Khomenko
Maciej Koutny


title: Generalized Symbolic Execution for Model Checking and Testing

authors:
Sarfraz Khurshid
Corina S. Pasareanu
Willem Visser


title: What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code


title: A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems


title: Automatic Abstraction without Counterexamples

authors:
Kenneth L. McMillan
Nina Amla


title: Using Petri Net Invariants in State Space Construction


title: Modeling and Analysis of Power-Aware Systems

authors:
Oleg Sokolsky
Anna Philippou
Insup Lee
Kyriakos Christou


title: Optimistic Synchronization-Based State-Space Reduction

authors:
Scott D. Stoller
Ernie Cohen


title: Automated Module Composition


title: LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios

authors:
Sebastián Uchitel
Robert Chatley
Jeff Kramer
Jeff Magee


title: Checking Properties of Heap-Manipulating Procedures with a Constraint Solver

authors:
Mandana Vaziri
Daniel Jackson


title: The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems

authors:
Dezhuang Zhang
Rance Cleaveland
Eugene W. Stark


title: Applying Game Semantics to Compositional Software Modeling and Verification

authors:
Samson Abramsky
Dan R. Ghica
Andrzej S. Murawski
C.-H. Luke Ong


title: Model Checking Discounted Temporal Properties

authors:
Luca de Alfaro
Marco Faella
Thomas A. Henzinger
Rupak Majumdar
Mariëlle Stoelinga


title: A Temporal Logic of Nested Calls and Returns

authors:
Rajeev Alur
Kousha Etessami
P. Madhusudan


title: Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes

authors:
Christel Baier
Boudewijn R. Haverkort
Holger Hermanns
Joost-Pieter Katoen


title: Refining Approximations in Software Predicate Abstraction

authors:
Thomas Ball
Byron Cook
Satyaki Das
Sriram K. Rajamani


title: Automatic Creation of Environment Models via Training

authors:
Thomas Ball
Vladimir Levin
Fei Xie


title: FASTer Acceleration of Counter Automata in Practice

authors:
Sébastien Bardin
Alain Finkel
Jérôme Leroux


title: Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic

authors:
Danièle Beauquier
Tristan Crolard
Evguenia Prokofieva


title: Lower and Upper Bounds in Zone Based Abstractions of Timed Automata

authors:
Gerd Behrmann
Patricia Bouyer
Kim Guldstrand Larsen
Radek Pelánek


title: Omega-Regular Model Checking

authors:
Bernard Boigelot
Axel Legay
Pierre Wolper


title: A Tool for Checking ANSI-C Programs

authors:
Edmund M. Clarke
Daniel Kroening
Flavio Lerda


title: Automatic Verification of Time Sensitive Cryptographic Protocols

authors:
Giorgio Delzanno
Pierre Ganty


title: SyncGen: An Aspect-Oriented Framework for Synchronization

authors:
Xianghua Deng
Matthew B. Dwyer
John Hatcliff
Masaaki Mizuno


title: Vooduu: Verification of Object-Oriented Designs Using UPPAAL

authors:
Karsten Diethers
Michaela Huhn


title: Liveness with Incomprehensible Ranking

authors:
Yi Fang
Nir Piterman
Amir Pnueli
Lenore D. Zuck


title: Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient

authors:
Jaco Geldenhuys
Antti Valmari


title: Numeric Domains with Summarized Dimensions

authors:
Denis Gopan
Frank DiMaio
Nurit Dor
Thomas W. Reps
Shmuel Sagiv


title: Error Explanation with Distance Metrics


title: Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points

authors:
Jan Friso Groote
Misa Keinänen


title: How Vacuous Is Vacuous?

authors:
Arie Gurfinkel
Marsha Chechik


title: Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata

authors:
Pavel Krcál
Wang Yi


title: From Complementation to Certification

authors:
Orna Kupferman
Moshe Y. Vardi


title: Revisiting Positive Equality

authors:
Shuvendu K. Lahiri
Randal E. Bryant
Amit Goel
Muralidhar Talupur


title: A Scalable Incomplete Test for the Boundedness of UML RT Models

authors:
Stefan Leue
Richard Mayr
Wei Wei


title: Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder

authors:
A. E. Lindsey
Charles Pecheur


title: Binding-Time Analysis for MetaML via Type Inference and Constraint Solving

authors:
Nathan Linger
Tim Sheard


title: A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata

authors:
Denis Lugiez
Peter Niebert
Sarah Zennou


title: Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method

authors:
Thomas Mailund
Michael Westergaard


title: An Interpolating Theorem Prover


title: MetaGame: An Animation Tool for Model-Checking Games

authors:
Markus Müller-Olm
Haiseung Yoo


title: The Succinct Solver Suite

authors:
Flemming Nielson
Hanne Riis Nielson
Hongyan Sun
Mikael Buchholtz
René Rydhof Hansen
Henrik Pilegaard
Helmut Seidl


title: CoPS - Checker of Persistent Security

authors:
Carla Piazza
Enrico Pivato
Sabina Rossi


title: Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases

authors:
Kairong Qian
Albert Nymeyer


title: Resource-Optimal Scheduling Using Priced Timed Automata

authors:
Jacob Illum Rasmussen
Kim Guldstrand Larsen
K. Subramani


title: Minimal Assignments for Bounded Model Checking

authors:
Kavita Ravi
Fabio Somenzi


title: Checking Strong Specifications Using an Extensible Software Model Checking Framework

authors:
Robby
Edwin Rodríguez
Matthew B. Dwyer
John Hatcliff


title: Automated Generation of a Progress Measure for the Sweep-Line Method


title: Online Efficient Predictive Safety Analysis of Multithreaded Programs

authors:
Koushik Sen
Grigore Rosu
Gul Agha


title: Monotonic Abstraction-Refinement for CTL

authors:
Sharon Shoham
Orna Grumberg


title: A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings

authors:
Zhendong Su
David A. Wagner


title: Tampere Verification Tool

authors:
Heikki Virtanen
Henri Hansen
Antti Valmari
Juha Nieminen
Timo Erkkilä


title: Symbolically Computing Most-Precise Abstract Operations for Shape Analysis

authors:
Greta Yorsh
Thomas W. Reps
Shmuel Sagiv