We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same complexity of the model checking problem for finite state models. Beyond this, we study the model checking problem of our logic for pushdown models. We argue that the combination of asynchronicity and a non-regular model class studied in this paper constitutes the first suitable approach for hyperproperty model checking against recursive programs.

We develop a generic framework to extend the logics LTL, CTL + and CTL ⁎ by automata-based connectives from formal language classes and analyse this framework with regard to regular languages, visibly pushdown languages, deterministic and non-deterministic context-free languages. More precisely, we consider how the use of different automata classes changes the expressive power of the logics and provide algorithms for the satisfiability and model checking problems induced by the use of different classes of automata. For the model checking problem, we treat not only finite Kripke transition systems, but also visibly pushdown systems and pushdown systems. We provide completeness or undecidability results in all cases and show that the extensions we consider can formulate properties not expressible in classical temporal logics or regular extensions thereof.

Hyperproperties have received increasing attention in the last decade due to their importance e.g. for security analyses. Past approaches have focussed on synchronous analyses, i.e. techniques in which different paths are compared lockstepwise. In this paper, we systematically study asynchronous analyses for hyperproperties by introducing both a novel automata model (Alternating Asynchronous Parity Automata) and the temporal fixpoint calculus H µ , the first fixpoint calculus that can systematically express hyperproperties in an asynchronous manner and at the same time subsumes the existing logic HyperLTL. We show that the expressive power of both models coincides over fixed path assignments. The high expressive power of both models is evidenced by the fact that decision problems of interest are highly undecidable, i.e. not even arithmetical. As a remedy, we propose approximative analyses for both models that also induce natural decidable fragments.

Information security properties of reactive systems like non-interference often require relating different executions of the system to each other and following them simultaneously. Such hyperproperties can also be useful in other contexts, e.g., when analysing properties of distributed systems like linearizability. Since common logics like LTL, CTL, or the modal mu-calculus cannot express hyperproperties, the hyperlogics HyperLTL and HyperCTL* were developed to cure this defect. However, these logics are not able to express arbitrary omega-regular properties. In this paper, we introduce HyperPDL-Delta, an adaptation of the Propositional Dynamic Logic of Fischer and Ladner for hyperproperties, in order to remove this limitation. Using an elegant automata-theoretic framework, we show that HyperPDL-Delta model checking is asymptotically not more expensive than HyperCTL* model checking, despite its vastly increased expressive power. We further investigate fragments of HyperPDL-Delta with regard to satisfiability checking.

We consider programs for embedded real-time systems which use priority-driven preemptive scheduling with task priorities adjusted dynamically according to the immediate ceiling priority protocol. For these programs, we provide static analyses for detecting data races between tasks running at different priorities as well as methods to guarantee transactional execution of procedures. Beyond that, we demonstrate how general techniques for value analyses can be adapted to this setting by developing a precise analysis of affine equalities.

In this article we provide an interprocedural analysis of linear two-variable equalities. The novel algorithm has a worst-case complexity of 𝒪( n ⋅ k 4 ), where k is the number of variables and n is the program size. Thus, it saves a factor of k 4 in comparison to a related algorithm based on full linear algebra. We also indicate how the practical runtime can be further reduced significantly. The analysis can be applied, for example, for register coalescing, for identifying local variables and thus for interprocedurally observing stack pointer modifications as well as for an analysis of array index expressions, when analyzing low-level code.

We consider integer arithmetic modulo a power of 2 as provided by mainstream programming languages like Java or standard implementations of C. The difficulty here is that, for w > 1, the ring Z m of integers modulo m = 2 w has zero divisors and thus cannot be embedded into a field. Not withstanding that, we present intra- and interprocedural algorithms for inferring for every program point u affine relations between program variables valid at u . If conditional branching is replaced with nondeterministic branching, our algorithms are not only sound but also complete in that they detect all valid affine relations in a natural class of programs. Moreover, they run in time linear in the program size and polynomial in the number of program variables and can be implemented by using the same modular integer arithmetic as the target language to be analyzed. We also indicate how our analysis can be extended to deal with equality guards, even in an interprocedural setting.

We apply linear algebra techniques to precise interprocedural dataflow analysis. Specifically, we describe analyses that determine for each program point identities that are valid among the program variables whenever control reaches that program point. Our analyses fully interpret assignment statements with affine expressions on the right hand side while considering other assignments as non-deterministic and ignoring conditions at branches. Under this abstraction, the analysis computes the set of all affine relations and, more generally, all polynomial relations of bounded degree precisely. The running time of our algorithms is linear in the program size and polynomial in the number of occurring variables. We also show how to deal with affine preconditions and local variables and indicate how to handle parameters and return values of procedures.

Optimal program slicing determines for a statement S in a program π whether or not S affects a specified set of statements, given that all conditionals in π are interpreted as non-deterministic choices.