38 citations · 133 across the 14 of their papers we have counts for
18 papers
Shelving it rather than Ditching it: Dynamically Debloating DEX and Native Methods of Android Applications without APK Modification
Zicheng Zhang, Jiakun Liu, Ferdian Thung +10
Today's Android developers tend to include numerous features to accommodate diverse user requirements, which inevitably leads to bloated apps. Yet more often than not, only a fract…
Unrealizable Cores for Reactive Systems Specifications
Shahar Maoz, Rafi Shalom
One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. One means…
Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games
Gal Amram, Shahar Maoz, Or Pistiner +1
-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of ve…
Spectra: A Specification Language for Reactive Systems
Shahar Maoz, Jan Oliver Ringert
Spectra is a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a k…
Performance Heuristics for GR(1) Synthesis and Related Algorithms
Elizabeth Firman, Shahar Maoz, Jan Oliver Ringert
Reactive synthesis for the GR(1) fragment of LTL has been implemented and studied in many works. In this workshop paper we present and evaluate a list of heuristics to potentially…
Symbolic BDD and ADD Algorithms for Energy Games
Shahar Maoz, Or Pistiner, Jan Oliver Ringert
Energy games, which model quantitative consumption of a limited resource, e.g., time or energy, play a central role in quantitative models for reactive systems. Reactive synthesis…
Synthesizing a Lego Forklift Controller in GR(1): A Case Study
Shahar Maoz, Jan Oliver Ringert
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. GR(1) is a well-known fragment of linear temporal logic…
A Manifesto for Semantic Model Differencing
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
Models are heavily used in software engineering and together with their systems they evolve over time. Thus, managing their changes is an important challenge for system maintainabi…
An Operational Semantics for Activity Diagrams using SMV
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
This document defines an operational semantics for activity diagrams (ADs) using a translation to SMV. The translation is inspired by the work of Eshuis [Esh06] and extends it with…
CDDiff: Semantic Differencing for Class Diagrams
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
Class diagrams (CDs), which specify classes and the relationships between them, are widely used for modeling the structure of object-oriented systems. As models, programs, and syst…
Modal Object Diagrams
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
While object diagrams (ODs) are widely used as a means to document object-oriented systems, they are expressively weak, as they are limited to describe specific possible snapshots…
ADDiff: Semantic Differencing for Activity Diagrams
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
Activity diagrams (ADs) have recently become widely used in the modeling of workflows, business processes, and web-services, where they serve various purposes, from documentation,…
CD2Alloy: Class Diagrams Analysis Using Alloy Revisited
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
We present CD2Alloy, a novel, powerful translation of UML class diagrams (CDs) to Alloy. Unlike existing translations, which are based on a shallow embedding strategy, and are thus…
Semantically Configurable Consistency Analysis for Class and Object Diagrams
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
Checking consistency between an object diagram (OD) and a class diagram (CD) is an important analysis problem. However, several variations in the semantics of CDs and ODs, as used…
Summarizing Semantic Model Differences
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
Fundamental building blocks for managing and understanding software evolution in the context of model-driven engineering are differencing operators one can use for model comparison…
An Interim Summary on Semantic Model Differencing
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
This position paper provides an interim summary on the goals and current state of our ongoing research project on semantic model differencing for software evolution. We describe th…
Synthesis of Component and Connector Models from Crosscutting Structural Views
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
We present component and connector (C&C) views, which specify structural properties of component and connector models in an expressive and intuitive way. C&C views provide means to…
Verifying Component and Connector Models against Crosscutting Structural Views
Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe
The structure of component and connector (C&C) models, which are used in many application domains of software engineering, consists of components at different containment levels, t…