title: Effective Soundness-Guided Reflection Analysis

authors:
Yue Li
Tian Tan
Jingling Xue

abstract: We introduce Solar, the first reflection analysis that allows its soundness to be reasoned about when some assumptions are met and produces significantly improved under-approximations otherwise. In both settings, Solar has three novel aspects: (1) lazy heap modeling for reflective allocation sites, (2) collective inference for improving the inferences on related reflective calls, and (3) automatic identification of “problematic” reflective calls that may threaten its soundness, precision and scalability, thereby enabling their improvement via lightweight annotations. We evaluate Solar against two state-of-the-art solutions, Doop and Elf, with the three treated as under-approximate reflection analyses, using 11 large Java benchmarks and applications. Solar is significantly more sound while achieving nearly the same precision and running only several-fold more slowly, subject to only 7 annotations in 3 programs.


venue: sas

title: A Simple Abstraction of Arrays and Maps by Program Translation

authors:
David Monniaux
Francesco Alberti

abstract: We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpretation, acceleration, predicate abstraction,...). The scalars invariants thus obtained are translated back onto the original program as universally quantified array invariants. We illustrate our approach on a variety of examples, leading to the “Dutch flag” algorithm.


title: Precise Data Flow Analysis in the Presence of Correlated Method Calls

authors:
Marianna Rapoport
Ondrej Lhoták
Frank Tip


title: Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR


title: Automated Verification of Linearization Policies

authors:
Parosh Aziz Abdulla
Bengt Jonsson
Cong Quy Trinh


title: Simulation and Invariance for Weak Consistency


title: Relational Verification Through Horn Clause Transformation

authors:
Emanuele De Angelis
Fabio Fioravanti
Alberto Pettorossi
Maurizio Proietti


title: Structure-Sensitive Points-To Analysis for C and C++

authors:
George Balatsouras
Yannis Smaragdakis

abstract: We present a points-to analysis for C/C++ that recovers much of the available high-level structure information of types and objects, by applying two key techniques: (1) It records the type of each abstract object and, in cases when the type is not readily available, the analysis uses an allocation-site plus type abstraction to create multiple abstract objects per allocation site, so that each one is associated with a single type. (2) It creates separate abstract objects that represent (a) the fields of objects of either struct or class type, and (b) the (statically present) constant indices of arrays, resulting in a limited form of array-sensitivity.


title: Quantitative Monitor Automata

authors:
Krishnendu Chatterjee
Thomas A. Henzinger
Jan Otop


title: Bounded Abstract Interpretation

authors:
Maria Christakis
Valentin Wüstholz


title: Securing a Compiler Transformation

authors:
Chaoqiang Deng
Kedar S. Namjoshi


title: Enforcing Termination of Interprocedural Analysis

authors:
Stefan Schulze Frielinghaus
Helmut Seidl
Ralf Vogler


title: Exploiting Sparsity in Difference-Bound Matrices

authors:
Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey


title: Flow- and Context-Sensitive Points-To Analysis Using Generalized Points-To Graphs

authors:
Pritam M. Gharat
Uday P. Khedker
Alan Mycroft


title: Learning a Variable-Clustering Strategy for Octagon from Labeled Data Generated by a Static Analysis

authors:
Kihong Heo
Hakjoo Oh
Hongseok Yang


title: Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Programs

authors:
Matthieu Journault
Antoine Miné


title: Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis

authors:
Kensuke Kojima
Minoru Kinoshita
Kohei Suenaga

abstract: The template-based method is one of the most successful approaches to algebraic invariant synthesis. In this method, an algorithm designates a template polynomial \(p\) over program variables, generates constraints for \(p=0\) to be an invariant, and solves the generated constraints. However, this approach often suffers from an increasing template size if the degree of a template polynomial is too high.


title: On the Linear Ranking Problem for Simple Floating-Point Loops

authors:
Fonenantsoa Maurica
Frédéric Mesnard
Étienne Payet


title: Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM

authors:
David Menendez
Santosh Nagarakatte
Aarti Gupta


title: A Parametric Abstract Domain for Lattice-Valued Regular Expressions

authors:
Jan Midtgaard
Flemming Nielson
Hanne Riis Nielson


title: Cell Morphing: From Array Programs to Array-Free Horn Clauses

authors:
David Monniaux
Laure Gonnord


title: Loopy: Programmable and Formally Verified Loop Transformations

authors:
Kedar S. Namjoshi
Nimit Singhania


title: Completeness in Approximate Transduction

authors:
Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni


title: Abstract Interpretation of Supermodular Games

abstract: Supermodular games are a well known class of noncooperative games which find significant applications in a variety of models, especially in operations research and economic applications. Supermodular games always have Nash equilibria which are characterized as fixed points of multivalued functions on complete lattices. Abstract interpretation is here applied to set up an approximation framework for Nash equilibria of supermodular games. This is achieved by extending the theory of abstract interpretation in order to cope with approximations of multivalued functions and by providing some methods for abstracting supermodular games, thus obtaining approximate Nash equilibria which are shown to be correct within the abstract interpretation framework.


title: Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants

authors:
Pierre Roux
Yuen-Lam Voronin
Sriram Sankaranarayanan


title: The Julia Static Analyzer for Java


title: From Array Domains to Abstract Interpretation Under Store-Buffer-Based Memory Models

authors:
Thibault Suzanne
Antoine Miné


title: Making k-Object-Sensitive Pointer Analysis More Precise with Still k-Limiting

authors:
Tian Tan
Yue Li
Jingling Xue

abstract: Object-sensitivity is regarded as arguably the best context abstraction for pointer analysis in object-oriented languages. However, a k-object-sensitive pointer analysis, which uses a sequence of k allocation sites (as k context elements) to represent a calling context of a method call, may end up using some context elements redundantly without inducing a finer partition of the space of (concrete) calling contexts for the method call. In this paper, we introduce Bean, a general approach for improving the precision of any k-object-sensitive analysis, denoted \(k\)-obj, by still using a k-limiting context abstraction. The novelty is to identify allocation sites that are redundant context elements in \(k\)-obj from an Object Allocation Graph (OAG), which is built based on a pre-analysis (e.g., a context-insensitive Andersen’s analysis) performed initially on a program and then avoid them in the subsequent k-object-sensitive analysis for the program. Bean is generally more precise than \(k\)-obj, with a precision that is guaranteed to be as good as \(k\)-obj in the worst case. We have implemented Bean as an open-source tool and applied it to refine two state-of-the-art whole-program pointer analyses in Doop. For two representative clients (may-alias and may-fail-cast) evaluated on a set of nine large Java programs from the DaCapo benchmark suite, Bean has succeeded in making both analyses more precise for all these benchmarks under each client at only small increases in analysis cost.


title: Probabilistic Horn Clause Verification


title: Combining Forward and Backward Abstract Interpretation of Horn Clauses

authors:
Alexey Bakhirkin
David Monniaux

abstract: Alternation of forward and backward analyses is a standard technique in abstract interpretation of programs, which is in particular useful when we wish to prove unreachability of some undesired program states. The current state-of-the-art technique for combining forward (bottom-up, in logic programming terms) and backward (top-down) abstract interpretation of Horn clauses is query-answer transformation. It transforms a system of Horn clauses, such that standard forward analysis can propagate constraints both forward, and backward from a goal. Query-answer transformation is effective, but has issues that we wish to address. For that, we introduce a new backward collecting semantics, which is suitable for alternating forward and backward abstract interpretation of Horn clauses. We show how the alternation can be used to prove unreachability of the goal and how every subsequent run of an analysis yields a refined model of the system. Experimentally, we observe that combining forward and backward analyses is important for analysing systems that encode questions about reachability in C programs. In particular, the combination that follows our new semantics improves the precision of our own abstract interpreter, including when compared to a forward analysis of a query-answer-transformed system.


title: Abstract Semantic Diffing of Evolving Concurrent Programs

authors:
Ahmed Bouajjani
Constantin Enea
Shuvendu K. Lahiri


title: Learning Shape Analysis

authors:
Marc Brockschmidt
Yuxin Chen
Pushmeet Kohli
Siddharth Krishna
Daniel Tarlow


title: Verifying Array Manipulating Programs by Tiling

authors:
Supratik Chakraborty
Ashutosh Gupta
Divyesh Unadkat

abstract: Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a novel property-driven verification method that first infers array access patterns in loops using simple heuristics, and then uses this information to compositionally prove universally quantified assertions about arrays. Specifically, we identify tiles of array accesses patterns in a loop, and use the tiling information to reduce the problem of checking a quantified assertion at the end of a loop to an inductive argument that checks only a slice of the assertion for a single iteration of the loop body. We show that this method can be extended to programs with sequentially composed loops and nested loops as well. We have implemented our method in a tool called Tiler. Initial experiments show that Tiler outperforms several state-of-the-art tools on a suite of interesting benchmarks.


title: Securing the SSA Transform

authors:
Chaoqiang Deng
Kedar S. Namjoshi


title: Relative Store Fragments for Singleton Abstraction

authors:
Leandro Facchinetti
Zachary Palmer
Scott F. Smith


title: Loop Invariants from Counterexamples

authors:
Marius Greitschus
Daniel Dietsch
Andreas Podelski


title: Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration


title: A Context-Sensitive Memory Model for Verification of C/C++ Programs

authors:
Arie Gurfinkel
Jorge A. Navas


title: Effect Summaries for Thread-Modular Analysis - Sound Analysis Despite an Unsound Heuristic

authors:
Lukás Holík
Roland Meyer
Tomás Vojnar
Sebastian Wolff

abstract: We propose a novel guess-and-check principle to increase the efficiency of thread-modular verification of lock-free data structures. We build on a heuristic that guesses candidates for stateless effect summaries of programs by searching the code for instances of a copy-and-check programming idiom common in lock-free data structures. These candidate summaries are used to compute the interference among threads in linear time. Since a candidate summary need not be a sound effect summary, we show how to fully automatically check whether the precision of candidate summaries is sufficient. We can thus perform sound verification despite relying on an unsound heuristic. We have implemented our approach and found it up to two orders of magnitude faster than existing ones.


title: Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models

authors:
Hernán Ponce de León
Florian Furbach
Keijo Heljanko
Roland Meyer


title: Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming

authors:
Alexandre Maréchal
David Monniaux
Michaël Périn


title: Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification

authors:
Isabella Mastroeni
Michele Pasqua


title: Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs

authors:
Suvam Mukherjee
Oded Padon
Sharon Shoham
Deepak D'Souza
Noam Rinetzky


title: Quantitative Static Analysis of Communication Protocols Using Abstract Markov Chains

authors:
Abdelraouf Ouadjaout
Antoine Miné


title: Template Polyhedra with a Twist

authors:
Sriram Sankaranarayanan
Mohamed Amin Ben Sassi


title: A New Abstraction Framework for Affine Transformers

authors:
Tushar Sharma
Thomas W. Reps


title: Synthesizing Imperative Programs from Examples Guided by Static Analysis

authors:
Sunbeom So
Hakjoo Oh


title: A Gradual Interpretation of Union Types

authors:
Matías Toro
Éric Tanter

abstract: Union types allow to capture the possibility of a term to be of several possibly unrelated types. Traditional static approaches to union types are untagged and tagged unions, which present dual advantages in their use. Inspired by recent work on using abstract interpretation to understand gradual typing, we present a novel design for union types, called gradual union types. Gradual union types combine the advantages of tagged and untagged union types, backed by dynamic checks. Seen as a gradual typing discipline, gradual union types are restricted imprecise types that denote a finite number of static types. We apply the Abstracting Gradual Typing (AGT) methodology of Garcia et al. to derive the static and dynamic semantics of a language that supports both gradual unions and the traditional, totally-unknown type. We uncover that gradual unions interact with the unknown type in a way that mandates a stratified approach to AGT, relying on a composition of two distinct abstract interpretations in order to retain optimality. Thanks to the abstract interpretation framework, the resulting language is type safe and satisfies the refined criteria for gradual languages. We also show how to compile such a language to a threesome cast calculus, and prove that the compilation preserves the semantics and properties of the language.


title: Modular Demand-Driven Analysis of Semantic Difference for Program Versions

authors:
Anna Trostanetski
Orna Grumberg
Daniel Kroening


title: Incremental Analysis for Probabilistic Programs

authors:
Jieyuan Zhang
Yulei Sui
Jingling Xue


title: Fairness: A Formal-Methods Perspective


title: Abstract Interpretation of Stateful Networks

authors:
Kalev Alpernas
Roman Manevich
Aurojit Panda
Mooly Sagiv
Scott Shenker
Sharon Shoham
Yaron Velner


title: Block-Size Independence for GPU Programs

authors:
Rajeev Alur
Joseph Devietti
Nimit Singhania


title: The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software

authors:
Roberto Bagnara
Abramo Bagnara
Patricia M. Hill

abstract: The MISRA project started in 1990 with the mission of providing world-leading best practice guidelines for the safe and secure application of both embedded control systems and standalone software. MISRA C is a coding standard defining a subset of the C language, initially targeted at the automotive sector, but now adopted across all industry sectors that develop C software in safety- and/or security-critical contexts. In this paper, we introduce MISRA C, its role in the development of critical software, especially in embedded systems, its relevance to industry safety standards, as well as the challenges of working with a general-purpose programming language standard that is written in natural language with a slow evolution over the last 40+ years. We also outline the role of static analysis in the automatic checking of compliance with respect to MISRA C, and the role of the MISRA C language subset in enabling a wider application of formal methods to industrial software written in C.


title: Extending Constraint-Only Representation of Polyhedra with Boolean Constraints

authors:
Alexey Bakhirkin
David Monniaux


title: An Efficient Abstract Domain for Not Necessarily Closed Polyhedra

authors:
Anna Becchi
Enea Zaffanella


title: Modular Software Fault Isolation as Abstract Interpretation

authors:
Frédéric Besson
Thomas P. Jensen
Julien Lepiller


title: Closing the Performance Gap Between Doubles and Rationals for Octagons

authors:
Aziem Chawdhary
Andy King


title: Verifying Properties of Differentiable Programs

authors:
Jan Hückelheim
Ziqing Luo
Sri Hari Krishna Narayanan
Stephen F. Siegel
Paul D. Hovland


title: A Reduced Product of Absolute and Relative Error Bounds for Floating-Point Analysis

authors:
Maxime Jacquemin
Sylvie Putot
Franck Védrine


title: Modular Static Analysis of String Manipulations in C Programs

authors:
Matthieu Journault
Antoine Miné
Abdelraouf Ouadjaout


title: Numerical Invariants via Abstract Machines


title: Verifying Bounded Subset-Closed Hyperproperties

authors:
Isabella Mastroeni
Michele Pasqua


title: Deductive Verification in Decidable Fragments with Ivy

authors:
Kenneth L. McMillan
Oded Padon


title: Process-Local Static Analysis of Synchronous Processes

authors:
Jan Midtgaard
Flemming Nielson
Hanne Riis Nielson


title: The Impact of Program Transformations on Static Program Analysis

authors:
Kedar S. Namjoshi
Zvonimir Pavlinovic


title: Experience Developing and Deploying Concurrency Analysis at Facebook


title: New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair


title: Efficiently Learning Safety Proofs from Appearance as well as Behaviours

authors:
Sumanth Prabhu
Kumar Madhukar
R. Venkatesh


title: Invertible Linear Transforms of Numerical Abstract Domains

authors:
Francesco Ranzato
Marco Zanella


title: Incremental Verification Using Trace Abstraction

authors:
Bat-Chen Rothenberg
Daniel Dietsch
Matthias Heizmann


title: Volume-Based Merge Heuristics for Disjunctive Numeric Domains

authors:
Andrew Ruef
Kesha Hietala
Arlen Cox


title: Interactive Verification of Distributed Protocols Using Decidable Logic


title: Abstract Interpretation of CTL Properties

authors:
Caterina Urban
Samuel Ueltschi
Peter Müller


title: Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction


title: Temporal Verification of Programs via First-Order Fixpoint Logic

authors:
Naoki Kobayashi
Takeshi Nishikawa
Atsushi Igarashi
Hiroshi Unno


title: Revisiting Polyhedral Analysis for Hybrid Systems


title: Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets

authors:
Amir M. Ben-Amram
Jesús J. Doménech
Samir Genaim

abstract: Multiphase ranking functions (M$\Phi$RFs) are tuples $\langle f_1,\ldots,f_d \rangle$ of linear functions that are often used to prove termination of loops in which the computation progresses through a number of "phases". Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (Single-Path Constraint loops). The decision problem existence of a M$\Phi$RF asks to determine whether a given SLC loop admits a M$\Phi$RF, and the corresponding bounded decision problem restricts the search to M$\Phi$RFs of depth $d$, where the parameter $d$ is part of the input. The algorithmic and complexity aspects of the bounded problem have been completely settled in a recent work. In this paper we make progress regarding the existence problem, without a given depth bound. In particular, we present an approach that reveals some important insights into the structure of these functions. Interestingly, it relates the problem of seeking M$\Phi$RFs to that of seeking recurrent sets (used to prove non-termination). It also helps in identifying classes of loops for which M$\Phi$RFs are sufficient. Our research has led to a new representation for single-path loops, the difference polyhedron replacing the customary transition polyhedron. This representation yields new insights on M$\Phi$RFs and SLC loops in general. For example, a result on bounded SLC loops becomes straightforward.


title: Abstract Interpretation of Indexed Grammars

authors:
Marco Campion
Mila Dalla Preda
Roberto Giacobazzi


title: Syntactic and Semantic Soundness of Structural Dataflow Analysis


title: Abstract Semantic Dependency


title: Analysis of Software Patches Using Numerical Abstract Interpretation

authors:
David Delmas
Antoine Miné


title: Responsibility Analysis by Abstract Interpretation

authors:
Chaoqiang Deng
Patrick Cousot

abstract: Given a behavior of interest in the program, statically determining the corresponding responsible entity is a task of critical importance, especially in program security. Classical static analysis techniques (e.g. dependency analysis, taint analysis, slicing, etc.) assist programmers in narrowing down the scope of responsibility, but none of them can explicitly identify the responsible entity. Meanwhile, the causality analysis is generally not pertinent for analyzing programs, and the structural equations model (SEM) of actual causality misses some information inherent in programs, making its analysis on programs imprecise. In this paper, a novel definition of responsibility based on the abstraction of event trace semantics is proposed, which can be applied in program security and other scientific fields. Briefly speaking, an entity ER is responsible for behavior B, if and only if ER is free to choose its input value, and such a choice is the first one that ensures the occurrence of B in the forthcoming execution. Compared to current analysis methods, the responsibility analysis is more precise. In addition, our definition of responsibility takes into account the cognizance of the observer, which, to the best of our knowledge, is a new innovative idea in program analysis.


title: On the Monniaux Problem in Abstract Interpretation

authors:
Nathanaël Fijalkow
Engel Lefaucheux
Pierre Ohlmann
Joël Ouaknine
Amaury Pouly
James Worrell


title: Language Inclusion Algorithms as Complete Abstract Interpretations

authors:
Pierre Ganty
Francesco Ranzato
Pedro Valero

abstract: We study the language inclusion problem \(L_1 \subseteq L_2\) where \(L_1\) is regular. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of \(L_1\), obtained by successively overapproximating the Kleene iterates of its least fixpoint characterization, is included in \(L_2\). We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e. its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e. it guarantees termination of least fixpoint computations). Such overapproximating abstraction function on languages can be defined using quasiorder relations on words where the abstraction gives the language of all words “greater than or equal to” a given input word for that quasiorder. We put forward a range of quasiorders that allow us to systematically design decision procedures for different language inclusion problems such as regular languages into regular languages or into trace sets of one-counter nets. In the case of inclusion between regular languages, some of the induced inclusion checking procedures correspond to well-known state-of-the-art algorithms like the so-called antichain algorithms. Finally, we provide an equivalent greatest fixpoint language inclusion check which relies on quotients of languages and, to the best of our knowledge, was not previously known.


title: Direct Manipulation for Imperative Programs

authors:
Qinheping Hu
Roopsha Samanta
Rishabh Singh
Loris D'Antoni


title: Fast and Precise Handling of Positive Weight Cycles for Field-Sensitive Pointer Analysis

authors:
Yuxiang Lei
Yulei Sui


title: Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification

authors:
Jianlin Li
Jiangchao Liu
Pengfei Yang
Liqian Chen
Xiaowei Huang
Lijun Zhang

abstract: Deep neural networks (DNNs) have been shown lack of robustness for the vulnerability of their classification to small perturbations on the inputs. This has led to safety concerns of applying DNNs to safety-critical domains. Several verification approaches have been developed to automatically prove or disprove safety properties of DNNs. However, these approaches suffer from either the scalability problem, i.e., only small DNNs can be handled, or the precision problem, i.e., the obtained bounds are loose. This paper improves on a recent proposal of analyzing DNNs through the classic abstract interpretation technique, by a novel symbolic propagation technique. More specifically, the values of neurons are represented symbolically and propagated forwardly from the input layer to the output layer, on top of abstract domains. We show that our approach can achieve significantly higher precision and thus can prove more properties than using only abstract domains. Moreover, we show that the bounds derived from our approach on the hidden neurons, when applied to a state-of-the-art SMT based verification tool, can improve its performance. We implement our approach into a software tool and validate it over a few DNNs trained on benchmark datasets such as MNIST, etc.


title: Rethinking Static Analysis by Combining Discrete and Continuous Reasoning


title: Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants

authors:
Daniel Neider
Shambwaditya Saha
Pranav Garg
P. Madhusudan


title: A Temporal Logic for Higher-Order Functional Programs

authors:
Yuya Okuyama
Takeshi Tsukada
Naoki Kobayashi


title: Robustness Verification of Support Vector Machines

abstract: We study the problem of formally verifying the robustness to adversarial examples of support vector machines (SVMs), a major machine learning model for classification and regression tasks. Following a recent stream of works on formal robustness verification of (deep) neural networks, our approach relies on a sound abstract version of a given SVM classifier to be used for checking its robustness. This methodology is parametric on a given numerical abstraction of real values and, analogously to the case of neural networks, needs neither abstract least upper bounds nor widening operators on this abstraction. The standard interval domain provides a simple instantiation of our abstraction technique, which is enhanced with the domain of reduced affine forms, which is an efficient abstraction of the zonotope abstract domain. This robustness verification technique has been fully implemented and experimentally evaluated on SVMs based on linear and nonlinear (polynomial and radial basis function) kernels, which have been trained on the popular MNIST dataset of images and on the recent and more challenging Fashion-MNIST dataset. The experimental results of our prototype SVM robustness verifier appear to be encouraging: this automated verification is fast, scalable and shows significantly high percentages of provable robustness on the test set of MNIST, in particular compared to the analogous provable robustness of neural networks.


title: Static Analysis of Data Science Software


title: A Change-Based Heuristic for Static Analysis with Policy Iteration

authors:
Marcus Völker
Stefan Kowalewski


title: Per-Dereference Verification of Temporal Heap Safety via Adaptive Context-Sensitive Analysis

authors:
Hua Yan
Shiping Chen
Yulei Sui
Yueqian Zhang
Changwei Zou
Jingling Xue


title: Verifying Numerical Programs via Iterative Abstract Testing

authors:
Banghu Yin
Liqian Chen
Jiangchao Liu
Ji Wang
Patrick Cousot


title: An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection

authors:
Hang Yu
David Monniaux

abstract: Polyhedral projection is a main operation of the polyhedron abstract domain. It can be computed via parametric linear programming (PLP), which is more efficient than the classic Fourier-Motzkin elimination method.


title: Farkas-Based Tree Interpolation

authors:
Sepideh Asadi
Martin Blicha
Antti E. J. Hyvärinen
Grigory Fedyukovich
Natasha Sharygina


title: On Multi-language Abstraction - Towards a Static Analysis of Multi-language Programs

authors:
Samuele Buro
Roy L. Crole
Isabella Mastroeni


title: Static Resource Analysis at Scale (Extended Abstract)

authors:
Ezgi Çiçek
Mehdi Bouaziz
Sungkeun Cho
Dino Distefano


title: Exact and Linear-Time Gas-Cost Analysis

authors:
Ankush Das
Shaz Qadeer


title: Termination of Polynomial Loops

authors:
Florian Frohn
Marcel Hark
Jürgen Giesl


title: Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries

authors:
Hugo Illous
Matthieu Lemerre
Xavier Rival


title: Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking

authors:
Naoki Iwayama
Naoki Kobayashi
Ryota Suzuki
Takeshi Tsukada


title: Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis

authors:
Anastasiia Izycheva
Eva Darulova
Helmut Seidl

abstract: Abstract We present an automated procedure for synthesizing sound inductive invariants for floating-point numerical loops. Our procedure generates invariants of the form of a convex polynomial inequality that tightly bounds the values of loop variables. Such invariants are a prerequisite for reasoning about the safety and roundoff errors of floating-point programs. Unlike previous approaches that rely on policy iteration, linear algebra or semi-definite programming, we propose a heuristic procedure based on simulation and counterexample-guided refinement. We observe that this combination is remarkably effective and general and can handle both linear and nonlinear loop bodies, nondeterministic values as well as conditional statements. Our evaluation shows that our approach can efficiently synthesize loop invariants for existing benchmarks from literature, but that it is also able to find invariants for nonlinear loops that today’s tools cannot handle.


title: Memory-Efficient Fixpoint Computation

authors:
Sung Kook Kim
Arnaud J. Venet
Aditya V. Thakur


title: Probabilistic Lipschitz Analysis of Neural Networks

authors:
Ravi Mangal
Kartik Sarangmath
Aditya V. Nori
Alessandro Orso


title: Simple and Efficient Computation of Minimal Weak Control Closure


title: Stratified Guarded First-Order Transition Systems

authors:
Christan Müller
Helmut Seidl

abstract: Abstract First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, stratification and guardedness. While guardedness represents a particular pattern how input predicates control existential quantifiers, stratification limits the information flow between predicates. Guardedness implies that the weakest precondition for every universal invariant is again universal, while the remaining sufficient criteria enforce that either the number of first-order variables, or the number of required instances of input predicates remains bounded, or the number of occurring negated literals decreases in every iteration. We argue for each of these three cases that termination of the fixpoint iteration can be guaranteed.


title: A Library Modeling Language for the Static Analysis of C Programs

authors:
Abdelraouf Ouadjaout
Antoine Miné


title: Cost Analysis of Smart Contracts Via Parametric Resource Analysis

authors:
Victor Perez-Carrasco
Maximiliano Klemen
Pedro López-García
José Francisco Morales
Manuel V. Hermenegildo

abstract: . The very nature of smart contracts and blockchain platforms, where program execution and storage are replicated across a large number of nodes, makes resource consumption analysis highly relevant. This has led to the development of analyzers for speciﬁc platforms and languages. However, blockchain platforms present signiﬁcant variability in languages and cost models, as well as over time. Approaches that facilitate the quick development and adaptation of cost analyses are thus potentially attractive in this context. We explore the application of a generic approach and tool for cost analysis to the problem of static inference of gas consumption bounds in smart contracts. The approach is based on Parametric Resource Analysis , a method that simpliﬁes the implementation of analyzers for inferring safe bounds on diﬀerent resources and with diﬀerent resource consumption models. In addition, to support diﬀerent input languages, the approach also makes use of translation into a Horn clause-based intermediate representation. To assess practicality we develop an analyzer for the Tezos platform and its Michelson language. We argue that this approach oﬀers a rapid, ﬂex-ible, and eﬀective method for the development of cost analyses for smart contracts.


title: Formal Framework for Reasoning About the Precision of Dynamic Analysis

authors:
Mila Dalla Preda
Roberto Giacobazzi
Niccolò Marastoni


title: Abstract Neural Networks

authors:
Matthew Sotoudeh
Aditya V. Thakur

abstract: Deep Neural Networks (DNNs) are rapidly being applied to safety-critical domains such as drone and airplane control, motivating techniques for verifying the safety of their behavior. Unfortunately, DNN verification is NP-hard, with current algorithms slowing exponentially with the number of nodes in the DNN. This paper introduces the notion of Abstract Neural Networks (ANNs), which can be used to soundly overapproximate DNNs while using fewer nodes. An ANN is like a DNN except weight matrices are replaced by values in a given abstract domain. We present a framework parameterized by the abstract domain and activation functions used in the DNN that can be used to construct a corresponding ANN. We present necessary and sufficient conditions on the DNN activation functions for the constructed ANN to soundly over-approximate the given DNN. Prior work on DNN abstraction was restricted to the interval domain and ReLU activation function. Our framework can be instantiated with other abstract domains such as octagons and polyhedra, as well as other activation functions such as Leaky ReLU, Sigmoid, and Hyperbolic Tangent.


title: Fast and Efficient Bit-Level Precision Tuning

authors:
Assalé Adjé
Dorra Ben Khalifa
Matthieu Martel

abstract: In this article, we introduce a new technique for precision tuning. This problem consists of finding the least data types for numerical values such that the result of the computation satisfies some accuracy requirement. State of the art techniques for precision tuning use a try and fail approach. They change the data types of some variables of the program and evaluate the accuracy of the result. Depending on what is obtained, they change more or less data types and repeat the process. Our technique is radically different. Based on semantic equations, we generate an Integer Linear Problem (ILP) from the program source code. Basically, this is done by reasoning on the most significant bit and the number of significant bits of the values which are integer quantities. The integer solution to this problem, computed in polynomial time by a (real) linear programming solver, gives the optimal data types at the bit level. A finer set of semantic equations is also proposed which does not reduce directly to an ILP problem. So we use policy iteration to find the solution. Both techniques have been implemented and we show that our results encompass the results of state of the art tools.


title: Hash Consed Points-To Sets

authors:
Mohamad Barbar
Yulei Sui


title: Data Abstraction: A General Framework to Handle Program Verification of Data Structures

authors:
Julien Braine
Laure Gonnord
David Monniaux


title: Backward Symbolic Execution with Loop Folding

authors:
Marek Chalupa
Jan Strejcek


title: Accelerating Program Analyses in Datalog by Merging Library Facts

authors:
Yifan Chen
Chenyang Yang
Xin Zhang
Yingfei Xiong
Hao Tang
Xiaoyin Wang
Lu Zhang


title: Static Analysis of Endian Portability by Abstract Interpretation

authors:
David Delmas
Abdelraouf Ouadjaout
Antoine Miné


title: Verified Functional Programming of an Abstract Interpreter

authors:
Lucas Franceschino
David Pichardie
Jean-Pierre Talpin

abstract: Abstract interpreters are complex pieces of software: even if the abstract interpretation theory and companion algorithms are well understood, their implementations are subject to bugs, that might question the soundness of their computations. While some formally verified abstract interpreters have been written in the past, writing and understanding them requires expertise in the use of proof assistants, and requires a non-trivial amount of interactive proofs. This paper presents a formally verified abstract interpreter fully programmed and proved correct in the F* verified programming environment. Thanks to F* refinement types and SMT prover capabilities we demonstrate a substantial saving in proof effort compared to previous works based on interactive proof assistants. Almost all the code of our implementation, proofs included, written in a functional style, are presented directly in the paper.


title: Disjunctive Interval Analysis

authors:
Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey


title: Static Analysis of ReLU Neural Networks with Tropical Polyhedra

authors:
Eric Goubault
Sébastien Palumby
Sylvie Putot
Louis Rustenholz
Sriram Sankaranarayanan

abstract: This paper studies the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. In this paper, we employ set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra. We show that tropical polyhedra can efficiently abstract ReLU activation function, while being able to control the loss of precision due to linear computations. We show how the connection between ReLU networks and tropical rational functions can provide approaches for range analysis of ReLU neural networks.


title: Exploiting Verified Neural Networks via Floating Point Numerical Error

authors:
Kai Jia
Martin C. Rinard

abstract: We show how to construct adversarial examples for neural networks with exactly verified robustness against $\ell_{\infty}$-bounded input perturbations by exploiting floating point error. We argue that any exact verification of real-valued neural networks must accurately model the implementation details of any floating point arithmetic used during inference or verification.


title: Verifying Low-Dimensional Input Neural Networks via Input Quantization

abstract: Deep neural networks are an attractive tool for compressing the control policy lookup tables in systems such as the Airborne Collision Avoidance System (ACAS). It is vital to ensure the safety of such neural controllers via verification techniques. The problem of analyzing ACAS Xu networks has motivated many successful neural network verifiers. These verifiers typically analyze the internal computation of neural networks to decide whether a property regarding the input/output holds. The intrinsic complexity of neural network computation renders such verifiers slow to run and vulnerable to floating-point error. This paper revisits the original problem of verifying ACAS Xu networks. The networks take low-dimensional sensory inputs with training data provided by a precomputed lookup table. We propose to prepend an input quantization layer to the network. Quantization allows efficient verification via input state enumeration, whose complexity is bounded by the size of the quantization space. Quantization is equivalent to nearest-neighbor interpolation at run time, which has been shown to provide acceptable accuracy for ACAS in simulation. Moreover, our technique can deliver exact verification results immune to floating-point error if we directly enumerate the network outputs on the target inference implementation or on an accurate simulation of the target implementation.


title: Toward Neural-Network-Guided Program Synthesis and Verification

authors:
Naoki Kobayashi
Taro Sekiyama
Issei Sato
Hiroshi Unno

abstract: We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks. Based on the idea, we have implemented a tool to synthesize formulas from positive/negative examples and implication constraints, and obtained promising experimental results. We also discuss two applications of our synthesis method. One is the use of our tool for qualifier discovery in the framework of ICE-learning-based CHC solving, which can in turn be applied to program verification and inductive invariant synthesis. Another application is to a new program development framework called oracle-based programming, which is a neural-network-guided variation of Solar-Lezama's program synthesis by sketching.


title: Selectively-Amortized Resource Bounding

authors:
Tianhan Lu
Bor-Yuh Evan Chang
Ashutosh Trivedi

abstract: We consider the problem of automatically proving resource bounds. That is, we study how to prove that an integer-valued resource variable is bounded by a given program expression. Automatic resource-bound analysis has recently received significant attention because of a number of important applications (e.g., detecting performance bugs, preventing algorithmic-complexity attacks, identifying side-channel vulnerabilities), where the focus has often been on developing precise amortized reasoning techniques to infer the most exact resource usage. While such innovations remain critical, we observe that fully precise amortization is not always necessary to prove a bound of interest. And in fact, by amortizing selectively, the needed supporting invariants can be simpler, making the invariant inference task more feasible and predictable. We present a framework for selectively-amortized analysis that mixes worst-case and amortized reasoning via a property decomposition and a program transformation. We show that proving bounds in any such decomposition yields a sound resource bound in the original program, and we give an algorithm for selecting a reasonable decomposition.


title: Selective Context-Sensitivity for k-CFA with CFL-Reachability

authors:
Jingbo Lu
Dongjie He
Jingling Xue


title: Reduced Products of Abstract Domains for Fairness Certification of Neural Networks

authors:
Denis Mazzucato
Caterina Urban


title: A Multilanguage Static Analysis of Python Programs with Native C Extensions

authors:
Raphaël Monat
Abdelraouf Ouadjaout
Antoine Miné


title: Automated Verification of the Parallel Bellman-Ford Algorithm

authors:
Mohsen Safari
Wytse Oortwijn
Marieke Huisman


title: Improving Thread-Modular Abstract Interpretation

authors:
Michael Schwarz
Simmo Saan
Helmut Seidl
Kalmer Apinis
Julian Erhard
Vesal Vojdani

abstract: We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a generalization of the analysis provided by the static analyzer Goblint as well as a natural improvement of Antoine Miné’s approach can be obtained as instances of this general scheme. We show that these two analyses are incomparable w.r.t. precision and provide a refinement which improves on both precision-wise. We also report on a preliminary experimental comparison of the given analyses on a meaningful suite of benchmarks.


title: Thread-Modular Analysis of Release-Acquire Concurrency

authors:
Divyanjali Sharma
Subodh Sharma

abstract: We present a thread-modular abstract interpretation(TMAI) technique to verify programs under the release-acquire (RA) memory model for safety property violations. The main contributions of our work are: we capture the execution order of program statements as an abstract domain, and propose a sound upper approximation over this domain to efficiently reason over RA concurrency. The proposed domain is general in its application and captures the ordering relations as a first-class feature in the abstract interpretation theory. In particular, the domain represents a set of sequences of modifications of a global variable in concurrent programs as a partially ordered set. Under this approximation, older sequenced-before stores of a global variable are forgotten and only the latest stores per variable are preserved. We establish the soundness of our proposed abstractions and implement them in a prototype abstract interpreter called PRIORI. The evaluations of PRIORI on existing and challenging RA benchmarks demonstrate that the proposed technique is not only competitive in refutation, but also in verification. PRIORI shows significantly fast analysis runtimes with higher precision compared to recent state-of-the-art tools for RA concurrency.


title: Symbolic Automatic Relations and Their Applications to SMT and CHC Solving

authors:
Takumi Shimoda
Naoki Kobayashi
Ken Sakayori
Ryosuke Sato

abstract: Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure under Boolean operations. We consider the satisfiability problem for SARs, and show that it is undecidable in general, but that we can construct a sound (but incomplete) and automated satisfiability checker by a reduction to CHC solving. We discuss applications to SMT and CHC solving on data structures, and show the effectiveness of our approach through experiments.


title: Compositional Verification of Smart Contracts Through Communication Abstraction

authors:
Scott Wesley
Maria Christakis
Jorge A. Navas
Richard J. Trefler
Valentin Wüstholz
Arie Gurfinkel

abstract: Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existing solutions either restrict the number of users to under-approximate behaviour, or rely on manual proofs. In this paper, we present local bundles that reduce contracts with arbitrarily many users to sequential programs with a few representative users. Each representative user abstracts concrete users that are locally symmetric to each other relative to the contract and the property. Our abstraction is semi-automated. The representatives depend on communication patterns, and are computed via static analysis. A summary for the behaviour of each representative is provided manually, but a default summary is often sufficient. Once obtained, a local bundle is amenable to sequential static analysis. We show that local bundles are relatively complete for parameterized safety verification, under moderate assumptions. We implement local bundle abstraction in SmartACE, and show order-of-magnitude speedups compared to a state-of-the-art verifier.


title: Automatic Synthesis of Data-Flow Analyzers

authors:
Xuezheng Xu
Xudong Wang
Jingling Xue


title: Solving Invariant Generation for Unsolvable Loops

authors:
Daneshvar Amrollahi
Ezio Bartocci
George Kenison
Laura Kovács
Marcel Moosbrugger
Miroslav Stankovic


title: Principles of Staged Static+Dynamic Partial Analysis

authors:
Aditya Anand
Manas Thakur


title: Specification-Guided Reinforcement Learning


title: Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs

authors:
Gilles Barthe
Adrien Koutsos
Solène Mirliaz
David Pichardie
Peter Schwabe


title: SecWasm: Information Flow Control for WebAssembly

authors:
Iulia Bastys
Maximilian Algehed
Alexander Sjösten
Andrei Sabelfeld


title: Lifting Numeric Relational Domains to Algebraic Data Types

authors:
Santiago Bautista
Thomas P. Jensen
Benoît Montagu


title: Automated Synthesis of Asynchronizations

authors:
Sidi Mohamed Beillahi
Ahmed Bouajjani
Constantin Enea
Shuvendu K. Lahiri


title: Case Study on Verification-Witness Validators: Where We Are and Where We Go

authors:
Dirk Beyer
Jan Strejcek

abstract: Abstract Software-verification tools sometimes produce incorrect answers, which can be a false alarm or a wrong claim of correctness. To increase the reliability of verification results, many verifiers now accompany their answers by witnesses in an interoperable standard format. There exist witness validators that can examine the witnesses and potentially confirm the verification results. This case study analyzes the quality of existing witness validators for C programs using the witnesses produced by a wide variety of 40 verification tools that participated in SV-COMP 2022. In particular, we show that many witness validators sometimes confirm witnesses that are invalid. To remedy this situation, we suggest some advances in witness validation, including a regular comparative evaluation of validators. Our suggestions were recently adopted by the SV-COMP community for the next edition of the competition.


title: Deciding Program Properties via Complete Abstractions on Bounded Domains

authors:
Roberto Bruni
Roberta Gori
Nicolas Manini


title: Invariant Inference with Provable Complexity from the Monotone Theory

authors:
Yotam M. Y. Feldman
Sharon Shoham


title: Efficient Modular SMT-Based Model Checking of Pointer Programs

authors:
Isabel Garcia-Contreras
Arie Gurfinkel
Jorge A. Navas


title: Property-Driven Code Obfuscations Reinterpreting Jones-Optimality in Abstract Interpretation

authors:
Roberto Giacobazzi
Isabella Mastroeni


title: Bootstrapping Library-Based Synthesis

authors:
Kangjing Huang
Xiaokang Qiu


title: Boosting Robustness Verification of Semantic Feature Neighborhoods

authors:
Anan Kabaha
Dana Drachsler-Cohen


title: Fast and Incremental Computation of Weak Control Closure


title: Local Completeness Logic on Kleene Algebra with Tests

authors:
Marco Milanese
Francesco Ranzato


title: Parameterized Recursive Refinement Types for Automated Program Verification

authors:
Ryoya Mukai
Naoki Kobayashi
Ryosuke Sato


title: Adversarial Logic


title: Towards Efficient Reasoning of Quantum Programs


title: CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial Attacks

authors:
Zhe Zhao
Yedi Zhang
Guangke Chen
Fu Song
Taolue Chen
Jiaxiang Liu


title: Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs

authors:
Rosa Abbasi
Eva Darulova


title: Unconstrained Variable Oracles for Faster Numeric Static Analyses

authors:
Vincenzo Arceri
Greta Dolcetti
Enea Zaffanella


title: Symbolic Transformation of Expressions in Modular Arithmetic

authors:
Jérôme Boillot
Jérôme Feret


title: A Formal Framework to Measure the Incompleteness of Abstract Interpretations

authors:
Marco Campion
Caterina Urban
Mila Dalla Preda
Roberto Giacobazzi


title: BREWasm: A General Static Binary Rewriting Framework for WebAssembly

authors:
Shangtong Cao
Ningyu He
Yao Guo
Haoyu Wang


title: Quantum Constant Propagation

authors:
Yanbin Chen
Yannick Stade

abstract: Abstract A quantum circuit is often executed on the initial state where each qubit is in the zero state. Therefore, we propose to perform a symbolic execution of the circuit. Our approach simulates groups of entangled qubits exactly up to a given complexity. Here, the complexity corresponds to the number of basis states expressing the quantum state of one entanglement group. By doing that, the groups need neither be determined upfront nor be bound by the number of involved qubits. Still, we ensure that the simulation runs in polynomial time - opposed to exponential time as required for the simulation of the entire circuit. The information made available at gates is exploited to remove superfluous controls and gates. We implemented our approach in the tool quantum constant propagation (QCP) and evaluated it on the circuits in the benchmark suite MQTBench. By applying our tool, only the work that cannot be carried out efficiently on a classical computer is left for the quantum computer, hence exploiting the strengths of both worlds.


title: Verifying Infinitely Many Programs at Once


title: Error Invariants for Fault Localization via Abstract Interpretation


title: Generalized Program Sketching by Abstract Interpretation and Logical Abduction


title: Mutual Refinements of Context-Free Language Reachability

authors:
Shuo Ding
Qirun Zhang


title: ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses

authors:
Florian Frohn
Jürgen Giesl


title: How Fitting is Your Abstract Domain?

authors:
Roberto Giacobazzi
Isabella Mastroeni
Elia Perantoni


title: A Product of Shape and Sequence Abstractions

authors:
Josselin Giet
Félix Ridoux
Xavier Rival


title: Error Localization for Sequential Effect Systems

authors:
Colin S. Gordon
Chaewon Yun


title: Scaling up Roundoff Analysis of Functional Data Structure Programs

authors:
Anastasia Isychev
Eva Darulova

abstract: Abstract Floating-point arithmetic is counter-intuitive due to inherent rounding errors that potentially occur at every arithmetic operation. A selection of automated tools now exists to ensure correctness of floating-point programs by computing guaranteed bounds on rounding errors at the end of a computation, but these tools effectively consider only straight-line programs over scalar variables. Much of numerical codes, however, use data structures such as lists, arrays or matrices and loops over these. To analyze such programs today, all data structure operations need to be unrolled, manually or by the analyzer, reducing the analysis to straight-line code, ultimately limiting the analyzers’ scalability. We present the first rounding error analysis for numerical programs written over vectors and matrices that leverages the data structure information to speed up the analysis. We facilitate this with our functional domain-specific input language that we design based on a new set of numerical benchmarks that we collect from a variety of domains. Our DSL explicitly carries semantic information that is useful for avoiding duplicate and thus unnecessary analysis steps, as well as enabling abstractions for further speed-ups. Compared to unrolling-based approaches in state-of-the-art tools, our analysis retains adequate accuracy and is able to analyze more benchmarks or is significantly faster, and particularly scales better for larger programs.


title: Abstract Interpretation in Industry - Experience and Lessons Learned

authors:
Daniel Kästner
Reinhard Wilhelm
Christian Ferdinand


title: Reverse Template Processing Using Abstract Interpretation


title: Domain Precision in Galois Connection-Less Abstract Interpretation

authors:
Isabella Mastroeni
Michele Pasqua


title: Lifting On-Demand Analysis to Higher-Order Languages

authors:
Daniel Schoepe
David Seekatz
Ilina Stoilkovska
Sandro Stucki
Daniel Tattersall
Pauline Bolignano
Franco Raimondi
Bor-Yuh Evan Chang


title: Octagons Revisited - Elegant Proofs and Simplified Algorithms

authors:
Michael Schwarz
Helmut Seidl

abstract: . Weakly relational domains have enjoyed tremendous success in the area of program analysis, since they oﬀer a decent compromise between precision and eﬃciency. Octagons , in particular, have widely been studied to obtain eﬃcient algorithms which, however, come with intricate correctness arguments. Here, we provide simpliﬁed cubic time algorithms for computing the closure of Octagon abstract relations both over the rationals and the integers which avoid introducing auxiliary variables. They are based on a more general formulation by means of 2 -projective domains which allows for an elegant short correctness proof. The notion of 2-projectivity also lends itself to eﬃcient algorithms for incremental normalization. For the Octagon domain, we also provide an improved construction for linear programming based best abstract transformers for aﬃne assignments.


title: Polynomial Analysis of Modular Arithmetic

authors:
Thomas Seed
Chris Coppins
Andy King
Neil Evans


title: Building Trust and Safety in Artificial Intelligence with Abstract Interpretation


title: Boosting Multi-neuron Convex Relaxation for Neural Network Verification

authors:
Xuezhou Tang
Ye Zheng
Jiaxiang Liu


title: Static Analysis of Quantum Programs

authors:
Nicola Assolini
Alessandra Di Pierro
Isabella Mastroeni


title: Trace Partitioning as an Optimization Problem

authors:
M. Charles Babu
Matthieu Lemerre
Sébastien Bardin
Jean-Yves Marion

abstract: . Imprecision is a very common phenomenon in static analyses that results in false alarms when used for program verification. Designing automatic techniques to improve static analysis precision is an old dream, but it is highly non-trivial. In the last two decades, static analysis gave rise to refinement techniques to improve precision through various forms of sensitivity. Yet, prior attempts are either specialized to particular domains or based on syntactic rules and heuristics that are tedious to design and prone to path explosion. In this paper, we cast the problem of improving static analysis precision as an optimization problem and propose a generic search-based method to solve it. We identify the challenges that one faces when solving this problem (like the large search space, path explosion, redundant computations, or non-monotonic operations in abstract domains) and provide adequate solutions to each. Finally, we provide a first implementation of the method, demonstrating both its feasibility and potential over standard benchmark (our early prototype is able to prove some goals that state-of-the-art software model checkers cannot), and providing valuable feedback when implementing this method in a static analyzer.


title: On the Role of Cognizance in Responsibility

authors:
Laura Canaia
Mila Dalla Preda


title: Lift-Offline: Instruction Lifter Generators

authors:
Nicholas Coughlin
Alistair Michael
Kait Lam


title: Full Control-Flow Sensitivity for Definitional Interpreters


title: Synthesizing Abstract Transformers for Reduced-Product Domains

authors:
Pankaj Kumar Kalita
Thomas W. Reps
Subhajit Roy


title: Abstract Interpretation of ReLU Neural Networks with Optimizable Polynomial Relaxations

authors:
Philipp Kern
Carsten Sinz


title: Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler

authors:
Julia Lawall
Keisuke Nishimura
Jean-Pierre Lozi


title: GoGuard: Efficient Static Blocking Bug Detection for Go

authors:
Bozhen Liu
Dhruti Joshi


title: Verification of Programs with ADTs Using Shallow Horn Clauses

authors:
Théo Losekoot
Thomas Genet
Thomas P. Jensen

abstract: This paper considers verification of relational properties of programs over algebraic data types (ADTs) by translating programs and properties into Constrained Horn clauses (CHCs). Verification reduces to satisfiability of CHCs modulo the theory of algebraic data types, which can be done by exhibiting a Herbrand model of the clauses. Herbrand models of CHCs with recursive ADTs are unbounded, so we need a formalism to finitely represent such models. We propose Shallow Horn Clauses (SHoCs), a new formalism for finitely representing unbounded Herbrand models. SHoCs enjoy the usual Boolean closure properties and are strictly more expressive and compact than tree automata and convoluted tree auto-mata, which have previously been used for this purpose. We propose an Implication CounterExample procedure (ICE) for inferring SHoCs. The model inference problem arising from relational verification is undecidable, so we propose an incomplete but sound inference procedure. Experiments show that this procedure performs well in practice w.r.t. state of the art tools, both for verifying properties and for finding counterexamples.


title: Quantitative Static Timing Analysis

authors:
Denis Mazzucato
Marco Campion
Caterina Urban


title: Under-Approximating Memory Abstractions

authors:
Marco Milanese
Antoine Miné


title: Robustness Verification of Multi-label Neural Network Classifiers

authors:
Julian Mour
Dana Drachsler-Cohen


title: An Order Theory Framework of Recurrence Equations for Static Cost Analysis - Dynamic Inference of Non-Linear Inequality Invariants

authors:
Louis Rustenholz
Pedro López-García
José F. Morales
Manuel V. Hermenegildo


title: Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel

authors:
Matan Shachnai
Harishankar Vishwanathan
Srinivas Narayana
Santosh Nagarakatte


title: ConstraintFlow: A Declarative DSL for Easy Development of DNN Certifiers

authors:
Avaljot Singh
Yasmin Sarita
Charith Mendis
Gagandeep Singh


title: BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code


title: Verifying Components of Arm® Confidential Computing Architecture with ESBMC

authors:
Tong Wu
Shale Xiong
Edoardo Manino
Gareth Stockwell
Lucas C. Cordeiro


title: Relating Distances and Abstractions - An Abstract Interpretation Perspective

authors:
Marco Campion
Isabella Mastroeni
Caterina Urban


title: A Programming Language for Feasible Solutions

authors:
Weijun Chen
Yuxi Fu
Huan Long

abstract: Runtime efficiency and termination are crucial properties in the studies of program verification. Instead of dealing with these issues in an ad hoc manner, it would be useful to develop a robust framework in which such properties are guaranteed by design. This paper introduces a new imperative programming language whose design is grounded in a static type system that ensures the following equivalence property: All definable programs are guaranteed to run in polynomial time; Conversely, all problems solvable in polynomial time can be solved by some programs of the language. The contribution of this work is twofold. On the theoretical side, the foundational equivalence property is established, and the proof of the equivalence theorem is non-trivial. On the practical side, a programming approach is proposed that can streamline program analysis and verification for feasible computations. An interpreter for the language has been implemented, demonstrating the feasibility of the approach in practice.


title: On a Simple Problem Due to Yves Bertot


title: Contextual Equality Saturation

authors:
Alexandre Drewery
Thomas P. Jensen
David Pichardie

abstract: . Equality saturation is a semantics-based technique for automatically and efficiently proving that two programs are equivalent modulo a fixed set of equality axioms. In this paper, we extend the equality saturation technique with contextual reasoning in order to perform rewriting under assumptions that are locally valid inside a conditional branch. This is based on a new notion of cyclic e-graphs with contextual annotations. We experimentally validate the efficiency and scalability of this new technique by proving equivalence of several families of programs where contextual reasoning is required.


title: Delta Store Semantics: Abstract Garbage Collection for Abstract Definitional Interpreters

authors:
Noah Van Es
Bram Vandenbogaerde
Coen De Roover


title: Ductape: Optimizing Dynamically Typed Programs Using Ahead-of-Time Compilation and Data-Flow Analysis

authors:
Adi Harif
Shachar Itzhaky


title: AURA: Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty

authors:
Zixin Huang
Jacob Laurel
Saikat Dutta
Sasa Misailovic


title: Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types

authors:
Hiroyuki Katsura
Naoki Kobayashi
Ken Sakayori
Ryosuke Sato


title: Formal Analysis of Networked PLC Controllers Interacting with Physical Environments

authors:
Jaeseo Lee
Kyungmin Bae


title: Verifying Neural Networks with PyRAT

authors:
Augustin Lemesle
Julien Lehmann
Tristan Le Gall
Zakaria Chihani


title: Comparing the Precision of Abstract Operators in the eBPF Verifier Using Differential Synthesis


title: Specifying and Verifying Future Conditions

authors:
Yahui Song
Darius Foo
Wei-Ngan Chin


title: Abstracting Concolic Execution for Soft Contract Verification

authors:
Bram Vandenbogaerde
Quentin Stiévenart
Coen De Roover


title: Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell

authors:
Bram Vandenbogaerde
Sarah Verbelen
Noah Van Es
Coen De Roover


title: Enhancing Neural Network Robustness via Synthesis of Repair Programs

authors:
Tom Yuviler
Dana Drachsler-Cohen


title: Bounded-Exhaustive Subspace Diversification for SMT Solver Testing

authors:
Junda Zheng
Peisen Yao


venue: sle

title: A Case Study in Grammar Engineering

authors:
Tiago L. Alves
Joost Visser


title: DeFacto: Language-Parametric Fact Extraction from Source Code

authors:
Hendrikus J. S. Basten
Paul Klint


title: Model-Driven Engineering Meets Generic Language Technology


title: Parse Table Composition

authors:
Martin Bravenboer
Eelco Visser


title: Engineering a DSL for Software Traceability

authors:
Nikolaos Drivalos
Dimitrios S. Kolovos
Richard F. Paige
Kiran Jude Fernandes

abstract: The software artefacts at different levels of abstraction and at different stages of the development process are closely inter-related. For developers to stay in control of the development process, traceability information must be maintained. In this paper, we present the engineering of the Traceability Metamodelling Language (TML), a metamodelling language dedicated to defining traceability metamodels. We present the abstract syntax of the language and its semantics, which are defined using a translational approach. Finally, we provide a case study that demonstrates the construction of a traceability metamodel that captures traceability information between two metamodels using TML.


title: Systematic Usage of Embedded Modelling Languages in Automated Model Transformation Chains

authors:
Mathias Fritzsche
Jendrik Johannes
Uwe Aßmann
Simon Mitschke
Wasif Gilani
Ivor T. A. Spence
T. John Brown
Peter Kilpatrick


title: Sudoku - A Language Description Case Study

authors:
Terje Gjøsæter
Ingelin F. Isfeldt
Andreas Prinz


title: Towards an Incremental Update Approach for Concrete Textual Syntaxes for UUID-Based Model Repositories


title: Transformation Language Integration Based on Profiles and Higher Order Transformations

authors:
Pieter Van Gorp
Anne Keller
Dirk Janssens


title: Neon: A Library for Language Usage Analysis

authors:
Jurriaan Hage
Peter van Keeken


title: The Java Programmer's Phrase Book

authors:
Einar W. Høst
Bjarte M. Østvold


title: The Field of Software Language Engineering


title: A Practical Evaluation of Using TXL for Model Transformation

authors:
Hongzhi Liang
Jürgen Dingel


title: Evaluating the Visual Syntax of UML: An Analysis of the Cognitive Effectiveness of the UMLFamily of Diagrams

authors:
Daniel L. Moody
Jos van Hillegersberg


title: Practical Scope Recovery Using Bridge Parsing

authors:
Emma Nilsson-Nyman
Torbjörn Ekman
Görel Hedin


title: Generating Rewritable Abstract Syntax Trees

authors:
Jeffrey L. Overbey
Ralph E. Johnson


title: Analyzing Rule-Based Behavioral Semantics of Visual Modeling Languages with Maude

authors:
José Eduardo Rivera
Esther Guerra
Juan de Lara
Antonio Vallecillo


title: Engineering Languages for Specifying Product-Derivation Processes in Software Product Lines

authors:
Pablo Sánchez
Neil Loughran
Lidia Fuentes
Alessandro Garcia


title: Formalization and Rule-Based Transformation of EMF Ecore-Based Models


title: A Model Engineering Approach to Tool Interoperability

authors:
Yu Sun
Zekai Demirezen
Frédéric Jouault
Robert Tairas
Jeff Gray


title: Composing Feature Models

authors:
Mathieu Acher
Philippe Collet
Philippe Lahire
Robert B. France


title: Multi-view Composition Language for Software Product Line Requirements

authors:
Mauricio Alférez
João Pedro Santos
Ana Moreira
Alessandro Garcia
Uirá Kulesza
João Araújo
Vasco Amaral


title: Yet Another Language Extension Scheme


title: Study of an API Migration for Two XML APIs

authors:
Thiago Tonelli Bartolomei
Krzysztof Czarnecki
Ralf Lämmel
Tijs van der Storm


title: Declarative Scripting in Haskell

authors:
Tim Bauer
Martin Erwig


title: If MDE Is the Solution, Then What Is the Problem?


title: Eating Our Own Dog Food: DSLs for Generative and Transformational Engineering


title: Integration of Data Validation and User Interface Concerns in a DSL for Web Applications

authors:
Danny M. Groenewegen
Eelco Visser


title: Closing the Gap between Modelling and Java

authors:
Florian Heidenreich
Jendrik Johannes
Mirko Seifert
Christian Wende


title: PIL: A Platform Independent Language for Retargetable DSLs

authors:
Zef Hemel
Eelco Visser


title: Language Evolution in Practice: The History of GMF

authors:
Markus Herrmannsdoerfer
Daniel Ratiu
Guido Wachsmuth


title: Model Transformation Languages Relying on Models as ADTs

authors:
Jerónimo Irazábal
Claudia Pons


title: Natural and Flexible Error Recovery for Generated Parsers

authors:
Maartje de Jonge
Emma Nilsson-Nyman
Lennart C. L. Kats
Eelco Visser


title: Generating Smart Wrapper Libraries for Arbitrary APIs


title: Graphical Template Language for Transformation Synthesis

authors:
Elina Kalnina
Audris Kalnins
Edgars Celms
Agris Sostaks


title: Ontological Metamodeling with Explicit Instantiation

authors:
Alfons Laarman
Ivan Kurtev


title: Towards Dynamic Evolution of Domain Specific Languages

authors:
Paul Laird
Stephen Barrett


title: A Novel Approach to Semi-automated Evolution of DSML Model Transformation

authors:
Tihamer Levendovszky
Daniel Balasubramanian
Anantha Narayanan
Gabor Karsai


title: An Automated Process for Implementing Multilevel Domain Models

authors:
Frédéric Mallet
François Lagarde
Charles André
Sébastien Gérard
François Terrier


title: Language Boxes

authors:
Lukas Renggli
Marcus Denker
Oscar Nierstrasz


title: Verifiable Parse Table Composition for Deterministic Parsing

authors:
August Schwerdfeger
Eric Van Wyk


title: ScalaQL: Language-Integrated Database Queries for Scala

authors:
Daniel Spiewak
Tian Zhao


title: A Role-Based Approach towards Modular Language Engineering

authors:
Christian Wende
Nils Thieme
Steffen Zschaler


title: Domain-Specific Metamodelling Languages for Software Language Engineering

authors:
Steffen Zschaler
Dimitrios S. Kolovos
Nikolaos Drivalos
Richard F. Paige
Awais Rashid


title: VML* - A Family of Languages for Variability Management in Software Product Lines

authors:
Steffen Zschaler
Pablo Sánchez
João Pedro Santos
Mauricio Alférez
Awais Rashid
Lidia Fuentes
Ana Moreira
João Araújo
Uirá Kulesza


title: The Level-Agnostic Modeling Language

authors:
Colin Atkinson
Bastian Kennel
Björn Goß


title: Feature and Meta-Models in Clafer: Mixed, Specialized, and Coupled

authors:
Kacper Bak
Krzysztof Czarnecki
Andrzej Wasowski


title: Extending DMM Behavior Specifications for Visual Execution and Debugging

authors:
Nils Bandener
Christian Soltenborn
Gregor Engels


title: DSLTrans: A Turing Incomplete Transformation Language

authors:
Bruno Barroca
Levi Lucio
Vasco Amaral
Roberto Félix
Vasco Sousa


title: Software Engineering and the Semantic Web: A Match Made in Heaven or in Hell?


title: Domain-Specific Modelling Languages with Algebraic Graph Transformations on RDF

authors:
Benjamin Braatz
Christoph Brandt


title: Reference Attribute Grammars for Metamodel Semantics

authors:
Christoff Bürger
Sven Karol
Christian Wende
Uwe Aßmann


title: JTL: A Bidirectional and Change Propagating Transformation Language

authors:
Antonio Cicchetti
Davide Di Ruscio
Romina Eramo
Alfonso Pierantonio


title: Featherweight TeX and Parser Correctness

authors:
Sebastian Thore Erdweg
Klaus Ostermann


title: A Language for Software Variation Research


title: Empirical Language Analysis in Software Linguistics

authors:
Jean-Marie Favre
Dragan Gasevic
Ralf Lämmel
Ekaterina Pek


title: Analysing the Cognitive Effectiveness of the BPMN 2.0 Visual Notation

authors:
Nicolas Genon
Patrick Heymans
Daniel Amyot


title: Subjective-C - Bringing Context to Mobile Platform Programming

authors:
Sebastián González
Nicolás Cardozo
Kim Mens
Alfredo Cádiz
Jean-Christophe Libbrecht
Julien Goffaux


title: COPE - A Workbench for the Coupled Evolution of Metamodels and Models


title: Metamodel Usage Analysis for Identifying Metamodel Improvements

authors:
Markus Herrmannsdoerfer
Daniel Ratiu
Maximilian Koegel


title: An Extensive Catalog of Operators for the Coupled Evolution of Metamodels and Models

authors:
Markus Herrmannsdoerfer
Sander Vermolen
Guido Wachsmuth


title: Canonical Method Names for Java - Using Implementation Semantics to Identify Synonymous Verbs

authors:
Einar W. Høst
Bjarte M. Østvold


title: Evaluating a Textual Feature Modelling Language: Four Industrial Case Studies

authors:
Arnaud Hubaux
Quentin Boucher
Herman Hartmann
Raphaël Michel
Patrick Heymans


title: Modelling GLL Parser Implementations

authors:
Adrian Johnstone
Elizabeth Scott

abstract: We describe the development of space-efficient implementations of GLL parsers, and the process by which we refine a set-theoretic model of the algorithm into a practical parser generator that creates practical parsers. GLL parsers are recursive descent-like, in that the structure of the parser's code closely mirrors the grammar rules, and so grammars (and their parsers) may be debugged by tracing the running parser in a debugger. While GLL recognisers are straightforward to describe, full GLL parsers present technical traps and challenges for the unwary. In particular, naive implementations based closely on the theoretical description of GLL can result in data structures that are not practical for grammars for real programming language grammars such as ANSI-C. We develop an equivalent formulation of the algorithm as a high-level set-theoretic model supported by table-based indices, in order to then explore a set of alternative implementations which trade space for time in ways which preserve the cubic bound.


title: Translator Generation Using ART


title: Interactive Disambiguation of Meta Programs with Concrete Object Syntax

authors:
Lennart C. L. Kats
Karl Trygve Kalleberg
Eelco Visser


title: Debugging in Domain-Specific Modelling

authors:
Raphael Mannadiar
Hans Vangheluwe


title: Support for the Evolution of C++ Generic Functions

authors:
Peter Pirkelbauer
Damian Dechev
Bjarne Stroustrup


title: Automated Co-evolution of GMF Editor Models

authors:
Davide Di Ruscio
Ralf Lämmel
Alfonso Pierantonio

abstract: The Eclipse Graphical Modeling (GMF) Framework provides the major approach for implementing visual languages on top of the Eclipse platform. GMF relies on a family of modeling languages to describe abstract syntax, concrete syntax as well as other aspects of the visual language and its implementation in an editor. GMF uses a model-driven approach to map the different GMF models to Java code. The framework, as it stands, lacks support for evolution. In particular, there is no support for propagating changes from the domain model (i.e., the abstract syntax of the visual language) to other editor models. We analyze the resulting co-evolution challenge, and we provide a solution by means of GMF model adapters, which automate the propagation of domain-model changes. These GMF model adapters are special model-to-model transformations that are driven by difference models for domain-model changes.


title: Automated Selective Caching for Reference Attribute Grammars

authors:
Emma Söderberg
Görel Hedin


title: A Unified Format for Language Documents

authors:
Vadim Zaytsev
Ralf Lämmel


title: Ambiguity Detection: Scaling to Scannerless

authors:
Hendrikus J. S. Basten
Paul Klint
Jurgen J. Vinju


title: Parse Forest Diagnostics with Dr. Ambiguity

authors:
Hendrikus J. S. Basten
Jurgen J. Vinju


title: Designing Variability Modeling Languages


title: Semantics First! - Rethinking the Language Design Process

authors:
Martin Erwig
Eric Walkingshaw


title: Comparison of Context-Free Grammars Based on Parsing Generated Test Data

authors:
Bernd Fischer
Ralf Lämmel
Vadim Zaytsev


title: RLSRunner: Linking Rascal with K for Program Analysis

authors:
Mark Hills
Paul Klint
Jurgen J. Vinju


title: Uniform Modularization of Workflow Concerns Using Unify

authors:
Niels Joncheere
Ragnhild Van Der Straeten


title: An Algorithm for Layout Preservation in Refactoring Transformations

authors:
Maartje de Jonge
Eelco Visser


title: Integrating Attribute Grammar and Functional Programming Language Features

authors:
Ted Kaminski
Eric Van Wyk


title: MoScript: A DSL for Querying and Manipulating Model Repositories

authors:
Wolfgang Kling
Frédéric Jouault
Dennis Wagelaar
Marco Brambilla
Jordi Cabot


title: Towards a One-Stop-Shop for Analysis, Transformation and Visualization of Software

authors:
Paul Klint
Bert Lisser
Atze van der Ploeg


title: Metacompiling OWL Ontologies

authors:
Anders Nilsson
Görel Hedin


title: Join Token-Based Event Handling: A Comprehensive Framework for Game Programming

authors:
Taketoshi Nishimori
Yasushi Kuno


title: An Architecture for Information Exchange Based on Reference Models

authors:
Heiko Paulheim
Daniel Oberle
Roland Plendl
Florian Probst


title: A Dedicated Language for Context Composition and Execution of True Black-Box Model Transformations

authors:
Andreas Seibel
Regina Hebig
Stefan Neumann
Holger Giese


title: Formalizing a Domain Specific Language Using SOS: An Industrial Case Study

authors:
Frank P. M. Stappers
Sven Weber
Michel A. Reniers
Suzana Andova
Istvan Nagy


title: Design of Concept Libraries for C++

authors:
Andrew Sutton
Bjarne Stroustrup


title: Cloning in DSLs: Experiments with OCL

authors:
Robert Tairas
Jordi Cabot


title: Reusing Pattern Solutions in Modeling: A Generic Approach Based on a Role Language

authors:
Christophe Tombelle
Gilles Vanwormhoudt
Emmanuel Renaux


title: Reconstructing Complex Metamodel Evolution

authors:
Sander Vermolen
Guido Wachsmuth
Eelco Visser


title: Towards Combinators for Bidirectional Model Transformations in Scala


title: Typed First-Class Communication Channels and Mobility for Concurrent Scripting Languages


title: TouchRAM: A Multitouch-Enabled Tool for Aspect-Oriented Software Design

authors:
Wisam Al Abed
Valentin Bonnet
Matthias Schöttle
Engin Yildirim
Omar Alam
Jörg Kienzle


title: Island Grammar-Based Parsing Using GLL and Tom

authors:
Ali Afroozeh
Jean-Christophe Bach
Mark van den Brand
Adrian Johnstone
Maarten Manders
Pierre-Etienne Moreau
Elizabeth Scott


title: A Framework for Bidirectional Model-to-Platform Transformations

authors:
Anthony Anjorin
Karsten Saller
Sebastian Rose
Andy Schürr


title: PAPAGENO: A Parallel Parser Generator for Operator Precedence Grammars

authors:
Alessandro Barenghi
Ermes Viviani
Stefano Crespi Reghizzi
Dino Mandrioli
Matteo Pradella


title: Approaches and Tools for Implementing Type Systems in Xtext

authors:
Lorenzo Bettini
Dietmar Stoll
Markus Völter
Serano Colameo


title: Bridging the Chasm between Executable Metamodeling and Models of Computation

authors:
Benoît Combemale
Cécile Hardebolle
Christophe Jacquet
Frédéric Boulanger
Benoit Baudry


title: The Program Is the Model: Enabling Transformations@run.time

authors:
Jesús Sánchez Cuadrado
Esther Guerra
Juan de Lara


title: On the Reusable Specification of Non-functional Properties in DSLs

authors:
Francisco Durán
Steffen Zschaler
Javier Troya

abstract: Domain-specific languages (DSLs) are an important tool for effective system development. They provide concepts that are close to the problem domain and allow analysis as well as generation of full solution implementations. However, this comes at the cost of having to develop a new language for every new domain. To make their development efficient, we must be able to construct DSLs as much as possible from reusable building blocks. In this paper, we discuss how such building blocks can be constructed for the specification and analysis of a range of non-functional properties, such as, for example, throughput, response time, or reliability properties. We assume DSL semantics to be provided through a set of transformation rules, which enables a range of analyses based on model checking. We demonstrate new concepts for defining language modules for the specification of non-functional properties, show how these can be integrated with base DSL specifications, and provide a number of syntactic conditions that we prove maintain the semantics of the base DSL even in the presence of non-functional–property specifications.


title: Layout-Sensitive Generalized Parsing

authors:
Sebastian Erdweg
Tillmann Rendel
Christian Kästner
Klaus Ostermann


title: Model Transformation Co-evolution: A Semi-automatic Approach

authors:
Jokin García
Oscar Díaz
Maider Azanza


title: A Common Foundational Theory for Bridging Two Levels in Ontology-Driven Conceptual Modeling

authors:
Giancarlo Guizzardi
Veruska Zamborlini


title: Meta-language Support for Type-Safe Access to External Resources

authors:
Mark Hills
Paul Klint
Jurgen J. Vinju


title: Modular Well-Definedness Analysis for Attribute Grammars

authors:
Ted Kaminski
Eric Van Wyk


title: Temporal Constraint Support for OCL

authors:
Bilal Kanso
Safouan Taha


title: Declarative Name Binding and Scope Rules

authors:
Gabriël D. P. Konat
Lennart C. L. Kats
Guido Wachsmuth
Eelco Visser


title: Termination Analysis for Higher-Order Attribute Grammars

authors:
Lijesh Krishnan
Eric Van Wyk


title: Metamodelling for Grammarware Researchers

authors:
Richard F. Paige
Dimitrios S. Kolovos
Fiona A. C. Polack


title: Profile-Based Abstraction and Analysis of Attribute Grammar Evaluation


title: Grammatical Inference in Software Engineering: An Overview of the State of the Art

authors:
Andrew Stevenson
James R. Cordy


title: Addressing Cognitive and Social Challenges in Designing and Using Ontologies in the Biomedical Domain


title: Object Grammars

authors:
Tijs van der Storm
William R. Cook
Alex Loh


title: Guided Merging of Sequence Diagrams

authors:
Magdalena Widl
Armin Biere
Petra Brosch
Uwe Egly
Marijn Heule
Gerti Kappel
Martina Seidl
Hans Tompits


title: Safe Specification of Operator Precedence Rules

authors:
Ali Afroozeh
Mark van den Brand
Adrian Johnstone
Elizabeth Scott
Jurgen J. Vinju


title: A Generic Framework for Symbolic Execution

authors:
Andrei Arusoaie
Dorel Lucanu
Vlad Rusu


title: A Pretty Good Formatting Pipeline

authors:
Anya Helene Bagge
Tero Hasu


title: Partial Instances via Subclassing

authors:
Kacper Bak
Zinovy Diskin
Michal Antkiewicz
Krzysztof Czarnecki
Andrzej Wasowski


title: Dark Knowledge and Graph Grammars in Automated Software Design

authors:
Don S. Batory
Rui C. Gonçalves
Bryan Marker
Janet Siegmund


title: Reifying Concurrency for Executable Metamodeling

authors:
Benoît Combemale
Julien De Antoni
Matias Vara Larsen
Frédéric Mallet
Olivier Barais
Benoit Baudry
Robert B. France


title: A Model-Driven Approach to Enhance Tool Interoperability Using the Theory of Models of Computation

authors:
Papa Issa Diallo
Joël Champeau
Loïc Lagadec


title: Mapping-Aware Megamodeling: Design Patterns and Laws

authors:
Zinovy Diskin
Sahar Kokaly
Tom Maibaum


title: The State of the Art in Language Workbenches - Conclusions from the Language Workbench Challenge

authors:
Sebastian Erdweg
Tijs van der Storm
Markus Völter
Meinte Boersma
Remi Bosman
William R. Cook
Albert Gerritsen
Angelo Hulshout
Steven Kelly
Alex Loh
Gabriël D. P. Konat
Pedro J. Molina
Martin Palatnik
Risto Pohjonen
Eugen Schindler
Klemens Schindler
Riccardo Solmi
Vlad A. Vergu
Eelco Visser
Kevin van der Vlist
Guido Wachsmuth
Jimi van der Woning


title: Software Evolution to Domain-Specific Languages

authors:
Stefan Fehrenbach
Sebastian Erdweg
Klaus Ostermann


title: Micro-Machinations - A DSL for Game Economies

authors:
Paul Klint
Riemer van Rozen


title: Method and Tool Support for Classifying Software Languages with Wikipedia

authors:
Ralf Lämmel
Dominik Mosen
Andrei Varanovich


title: xMOF: Executable DSMLs Based on fUML

authors:
Tanja Mayerhofer
Philip Langer
Manuel Wimmer
Gerti Kappel


title: Whiley: A Platform for Research in Software Verification

authors:
David J. Pearce
Lindsay Groves


title: Developing a Domain-Specific Language for Scheduling in the European Energy Sector

authors:
Stefan Sobernig
Mark Strembeck
Andreas Beck


title: Circular Higher-Order Reference Attribute Grammars

authors:
Emma Söderberg
Görel Hedin


title: Variability Support in Domain-Specific Language Development

authors:
Edoardo Vacchi
Walter Cazzola
Suresh Pillay
Benoît Combemale


title: Detecting Ambiguity in Programming Language Grammars

authors:
Naveneetha Vasudevan
Laurence Tratt


title: A Language Independent Task Engine for Incremental Name and Type Analysis

authors:
Guido Wachsmuth
Gabriël D. P. Konat
Vlad A. Vergu
Danny M. Groenewegen
Eelco Visser


title: Micropatterns in Grammars

abstract: Micropatterns and nanopatterns have been previously demonstrated to be useful techniques for object-oriented program comprehension. In this paper, we use a similar approach for identifying structurally similar fragments in grammars in a broad sense (contracts for commitment to structure), in particular parser specifications, metamodels and data models. Grammatical micropatterns bridge the gap between grammar metrics, which are easy to implement but hard to assign meaning to, and language design guidelines, which are inherently meaningful as stemming from current software language engineering practice but considerably harder to formalise.


title: Model Checking of CTL-Extended OCL Specifications

authors:
Robert Bill
Sebastian Gabmeyer
Petra Kaufmann
Martina Seidl


title: The Moldable Debugger: A Framework for Developing Domain-Specific Debuggers

authors:
Andrei Chis
Tudor Gîrba
Oscar Nierstrasz


title: Eco: A Language Composition Editor

authors:
Lukas Diekmann
Laurence Tratt


title: Unifying and Generalizing Relations in Role-Based Data Modeling and Navigation

authors:
Daco Harkes
Eelco Visser


title: Test-Data Generation for Xtext - Tool Paper

authors:
Johannes Härtel
Lukas Härtel
Ralf Lämmel


title: Streamlining Control Flow Graph Construction with DCFlow


title: Evaluating the Usability of a Visual Feature Modeling Notation

authors:
Aleksandar Jaksic
Robert B. France
Philippe Collet
Sudipto Ghosh

abstract: Feature modeling is a popular Software Product Line Engineering (SPLE) technique used to describe variability in a product family. A usable feature modeling tool environment should enable SPLE practitioners to produce good quality models, in particular, models that effectively communicate modeled information. FAMILIAR is a text-based environment for manipulating and composing Feature Models (FMs). In this paper we present extensions we made to FAMILIAR to enhance its usability. The extensions include a visualization of FMs, or more precisely, a feature diagram rendering mechanism that supports the use of a combination of text and graphics to describe FMs, their configurations, and the results of FM analyses. We also present the results of a preliminary evaluation of the environment’s usability. The evaluation involves comparing the use of the extended environment with the previous text-based console-driven version. The preliminary experiment provides some evidence that use of the new environment results in increased cognitive effectiveness of novice users and improved quality of new FMs.


title: Dynamic Scope Discovery for Model Transformations

authors:
Maris Jukss
Clark Verbrugge
Dániel Varró
Hans Vangheluwe


title: A SAT-Based Debugging Tool for State Machines and Sequence Diagrams

authors:
Petra Kaufmann
Martin Kronegger
Andreas Pfandler
Martina Seidl
Magdalena Widl


title: A Metamodel Family for Role-Based Modeling and Programming Languages

authors:
Thomas Kühn
Max Leuthäuser
Sebastian Götz
Christoph Seidl
Uwe Aßmann


title: Bounded Seas - - Island Parsing Without Shipwrecks

authors:
Jan Kurs
Mircea Lungu
Oscar Nierstrasz


title: ProMoBox: A Framework for Generating Domain-Specific Property Languages

authors:
Bart Meyers
Romuald Deshayes
Levi Lucio
Eugene Syriani
Hans Vangheluwe
Manuel Wimmer


title: AIOCJ: A Choreographic Framework for Safe Adaptive Distributed Applications

authors:
Mila Dalla Preda
Saverio Giallorenzo
Ivan Lanese
Jacopo Mauro
Maurizio Gabbrielli

abstract: We present AIOCJ, a framework for programming distributed adaptive applications. Applications are programmed using AIOC, a choreographic language suited for expressing patterns of interaction from a global point of view. AIOC allows the programmer to specify which parts of the application can be adapted. Adaptation takes place at runtime by means of rules, which can change during the execution to tackle possibly unforeseen adaptation needs. AIOCJ relies on a solid theory that ensures applications to be deadlock-free by construction also after adaptation. We describe the architecture of AIOCJ, the design of the AIOC language, and an empirical validation of the framework.


title: Simple, Efficient, Sound and Complete Combinator Parsing for All Context-Free Grammars, Using an Oracle

abstract: Parsers for context-free grammars can be implemented directly and naturally in a functional style known as “combinator parsing”, using recursion following the structure of the grammar rules. Traditionally parser combinators have struggled to handle all features of context-free grammars, such as left recursion.


title: Monto: A Disintegrated Development Environment

authors:
Anthony M. Sloane
Matthew Roberts
Scott Buckley
Shaun Muscat


title: Respect Your Parents: How Attribution and Rewriting Can Get Along

authors:
Anthony M. Sloane
Matthew Roberts
Leonard G. C. Hamey


title: fUML as an Assembly Language for Model Transformation

authors:
Massimo Tisi
Frédéric Jouault
Jérôme Delatour
Zied Saidi
Hassene Choura


title: Towards User-Friendly Projectional Editors

authors:
Markus Völter
Janet Siegmund
Thorsten Berger
Bernd Kolb


title: Origin Tracking in Attribute Grammars

authors:
Kevin Williams
Eric Van Wyk


title: A combined formal model for relational context-dependent roles

authors:
Thomas Kühn
Stephan Böhme
Sebastian Götz
Uwe Aßmann

abstract: Role-based modeling has been investigated for over 35 years as a promising paradigm to model complex, dynamic systems. Although current software systems are characterized by increasing complexity and context-dependence, all this research had almost no influence on current software development practice, still being discussed in recent literature. One reason for this is the lack of a coherent, comprehensive, readily applicable notion of roles. Researchers focused either on relational roles or context-dependent roles rather then combining both natures. Currently, there is no role-based modeling language sufficiently incorporating both the relational and context-dependent nature of roles together with the various proposed constraints. Hence, this paper formalizes a full-fledged role-based modeling language supporting both natures. To show its sufficiency and adequacy, a real world example is employed.


title: Analysis and transformation with the nuthatch tree-walking library

abstract: Nuthatch is a system for traversing, collecting information from, and rewriting trees, based on the idea of tree walking. The main application is software analysis and transformation. Nuthatch traversals are non-recursive by default and independent of the concrete tree representation. We provide an extensible library, Nuthatch/J, for doing tree walking in Java, with adapters for interfacing with popular software transformation tools like Stratego/XT and Rascal. Transformations are described as walks that proceed in programmer-defined steps. Each step can perform actions based on observed properties of current node and walk, and affect state associated with the walk and also rewrite the walked tree. A step ends by walking to a different node in the tree, following the tree branches, and the walk ends by returning to the top.


title: Distributed model-to-model transformation with ATL on MapReduce

authors:
Amine Benelallam
Abel Gómez
Massimo Tisi
Jordi Cabot

abstract: Efficient processing of very large models is a key requirement for the adoption of Model-Driven Engineering (MDE) in some industrial contexts. One of the central operations in MDE is rule-based model transformation (MT). It is used to specify manipulation operations over structured data coming in the form of model graphs. However, being based on computationally expensive operations like subgraph isomorphism, MT tools are facing issues on both memory occupancy and execution time while dealing with the increasing model size and complexity. One way to overcome these issues is to exploit the wide availability of distributed clusters in the Cloud for the distributed execution of MT. In this paper, we propose an approach to automatically distribute the execution of model transformations written in a popular MT language, ATL, on top of a well-known distributed programming model, MapReduce. We show how the execution semantics of ATL can be aligned with the MapReduce computation model. We describe the extensions to the ATL transformation engine to enable distribution, and we experimentally demonstrate the scalability of this solution in a reverse-engineering scenario.


title: Supporting efficient and advanced omniscient debugging for xDSMLs

authors:
Erwan Bousse
Jonathan Corley
Benoît Combemale
Jeffrey G. Gray
Benoit Baudry

abstract: Omniscient debugging is a promising technique that relies on execution traces to enable free traversal of the states reached by a system during an execution. While some General-Purpose Languages (GPLs) already have support for omniscient debugging, developing such a complex tool for any executable Domain-Specific Modeling Language (xDSML) remains a challenging and error prone task. A solution to this problem is to define a generic omniscient debugger for all xDSMLs. However, generically supporting any xDSML both compromises the efficiency and the usability of such an approach. Our contribution relies on a partly generic omniscient debugger supported by generated domain-specific trace management facilities. Being domain-specific, these facilities are tuned to the considered xDSML for better efficiency. Usability is strengthened by providing multidimensional omniscient debugging. Results show that our approach is on average 3.0 times more efficient in memory and 5.03 more efficient in time when compared to a generic solution that copies the model at each step.


title: Reference attribute grammar controlled graph rewriting: motivation and overview

abstract: Reference attribute grammars are a well-known language engineering technique for the implementation of semantic analyses. Reference attributes provide declarative means to extend abstract syntax trees to graphs and analyse such graphs; they are well-suited to deduce and reason about abstract syntax graphs. Efficient attribute re-evaluation in case of abstract syntax graph changes and a systematic integration of attribute-based analyses with further rewrite-based transformations are open research problems however. To solve these problems, a novel incremental syntax-directed compiler-compiler technique is presented, that seamlessly combines reference attribute grammars and graph rewriting. The presented technique not only permits incremental reference attribute evaluation, but also the reuse of analyses to ease the specification of, and guide, rewrite-based transformations. It enables efficient, mutually dependent, memoized analyses and transformations. The paper motivates and explains the concepts of such a reference attribute grammar controlled graph rewriting. For evaluation, a reference implementation is used to specify fUML Activity Diagram and Petri net interpreters.


title: Melange: a meta-language for modular and reusable development of DSLs

authors:
Thomas Degueule
Benoît Combemale
Arnaud Blouin
Olivier Barais
Jean-Marc Jézéquel

abstract: Domain-Specific Languages (DSLs) are now developed for a wide variety of domains to address specific concerns in the development of complex systems. When engineering new DSLs, it is likely that previous efforts spent on the development of other languages could be leveraged, especially when their domains overlap. However, legacy DSLs may not fit exactly the end user requirements and thus require further extension, restriction, or specialization. While current language workbenches provide import mechanisms, they usually lack an explicit support for such customizations of imported artifacts. In this paper, we propose an approach for building DSLs by safely assembling and customizing legacy DSLs artifacts. This approach is based on typing relations that provide a reasoning layer for manipulating DSLs while ensuring type safety. On top of this reasoning layer, we provide an algebra of operators for extending, restricting, and assembling separate DSL artifacts. We implemented the typing relations and algebra into the Melange meta-language. We illustrate Melange through the modular definition of an executable modeling language for the Internet Of Things domain. We show how it eases the definition of new DSLs by maximizing the reuse of legacy artifacts without introducing issues in terms of performance, technical ecosystem compatibility, or generated code volume.