23 citations · 43 across the 10 of their papers we have counts for
7 papers · 1 filter
A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features (Extended Version)
Aleksandar S. Dimovski, Sven Apel, Axel Legay
Lifted (family-based) static analysis by abstract interpretation is capable of analyzing all variants of a program family simultaneously, in a single run without generating any of…
Variability Abstraction and Refinement for Game-based Lifted Model Checking of full CTL (Extended Version)
Aleksandar S. Dimovski, Axel Legay, Andrzej Wasowski
Variability models allow effective building of many custom model variants for various configurations. Lifted model checking for a variability model is capable of verifying all its…
Verification of High-Level Transformations with Inductive Refinement Types
Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar S. Dimovski +1
High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backt…
Probabilistic Analysis Based On Symbolic Game Semantics and Model Counting
Aleksandar S. Dimovski
Probabilistic program analysis aims to quantify the probability that a given program satisfies a required property. It has many potential applications, from program understanding a…
Effective Analysis of C Programs by Rewriting Variability
Alexandru Florin Iosif-Lazar, Jean Melo, Aleksandar S. Dimovski +2
Context. Variability-intensive programs (program families) appear in many application areas and for many reasons today. Different family members, called variants, are derived by sw…
Variability Abstractions: Trading Precision for Speed in Family-Based Analyses (Extended Version)
Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wąsowski
Family-based (lifted) data-flow analysis for Software Product Lines (SPLs) is capable of analyzing all valid products (variants) without generating any of them explicitly. It takes…
Slot Games for Detecting Timing Leaks of Programs
Aleksandar S. Dimovski
In this paper we describe a method for verifying secure information flow of programs, where apart from direct and indirect flows a secret information can be leaked through covert t…