Author name cluster

Markus Müller-Olm

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

I&C Journal 2023 Journal Article

Temporal logics with language parameters

Jens Oliver Gutsfeld
Markus Müller-Olm
Christian Dielitz

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.

Details DOI

LOPSTR Conference 2015 Conference Paper

Using Dynamic Pushdown Networks to Automate a Modular Information-Flow Analysis

Heiko Mantel
Markus Müller-Olm
Matthias Perner
Alexander Wenner

Abstract In this article, we propose a static information-flow analysis for multi-threaded programs with shared memory communication and synchronization via locks. In contrast to many prior analyses, our analysis does not only prevent information leaks due to synchronization, but can also benefit from synchronization for its precision. Our analysis is a novel combination of type systems and a reachability analysis based on dynamic pushdown networks. The security type system supports flow-sensitive tracking of security levels for shared variables in the analysis of one thread by exploiting assumptions about variable accesses by other threads. The reachability analysis based on dynamic pushdown networks verifies that these assumptions are sound using the result of an automatic guarantee inference. The combined analysis is the first automatic static analysis that supports flow-sensitive tracking of security levels while being sound with respect to termination-sensitive noninterference.

Details

LPAR Conference 2004 Conference Paper

A Generic Framework for Interprocedural Analyses of Numerical Properties

Markus Müller-Olm
Helmut Seidl

Abstract Relations among program variables like 1 + 3 · x 1 + 5 · x 2 ≡ 0 [224] have been called linear congruence relations. Such a relation is valid at a program point iff it is satisfied by all reaching program states. Knowledge about non-trivial valid congruence relations is crucial for various aggressive program transformations. It can also form the backbone of a program correctness proof. In his seminal paper [1], Philippe Granger presents an intraprocedural analysis which is able to infer linear congruence relations between integer variables. For affine programs, i. e. , programs where all assignments are affine expressions and branching is non-deterministic, Granger’s analysis is complete, i. e. , infers all valid congruence relations between variables. No upper bound, though, has been proven for Granger’s algorithm. Here, we present a variation of Granger’s analysis which runs in polynomial time. Moreover, we provide an interprocedural extension of this algorithm. The polynomial algorithm as well as its interprocedural extension are obtained by means of multiple instances of a general framework for constructing interprocedural analyses of numerical properties. This framework can be used for different numerical domains such as fields or modular rings and thus also covers the interprocedural analyses of [2, 3] where valid affine relations are inferred. We also indicate how the base technique can be extended to deal with equality guards in the interprocedural setting.

Details

TCS Journal 2004 Journal Article

Precise interprocedural dependence analysis of parallel programs

Markus Müller-Olm

It is known that interprocedural detection of copy constants and elimination of faint code in parallel programs are undecidable problems, if base statements are assumed to execute atomically. We show that these problems become decidable, if this assumption is abandoned. So, the (unrealistic) idealization from program verification “atomic execution of base statements” introduced in order to simplify matters, actually increases the difficulty of these problems from the point of view of program analysis: amazingly these problems become more tractable if we adopt a less idealized, more realistic model of execution. We introduce an effective abstract domain of antichains of dependence traces that allows us to perform a precise interprocedural dependence analysis in (non-atomically executing) parallel programs. The main idea is to trace sequences of dependences exhibited successively by program executions. We define operations on antichains of dependence traces and show that they precisely abstract the corresponding operations on sets of non-atomic program executions. Using these operations, we can analyze dependences by means of an abstract interpretation of constraint systems that characterize sets of program executions of interest. The result of the dependence analysis can in turn be used to detect all copy constants and to eliminate faint code. While the run-time of the algorithms is exponential in the number of program variables, it is polynomial in the program size. Hence, they are polynomial-time algorithms if the number of program variables is bounded. In order to justify their overall exponential run-time, we show that both detection of copy constants and elimination of faint code are intractable (NP-hard) even when the atomic execution idealization is abandoned. This holds already for parallel programs without loops or procedures.

Details DOI

LOPSTR Conference 2003 Conference Paper

Formal Development and Verification of Approximation Algorithms Using Auxiliary Variables

Rudolf Berghammer
Markus Müller-Olm

Abstract For many intractable optimization problems efficient approximation algorithms have been developed that return near-optimal solutions. We show how such algorithms and worst-case bounds for the quality of their results can be developed and verified as structured programs. The proposed method has two key steps. First, auxiliary variables are introduced that allow a formal analysis of the worst-case behavior. In a second step these variables are eliminated from the program and existential quantifiers are introduced in assertions. We show that the elimination procedure preserves validity of proofs and illustrate the approach by two examples.

Details

STOC Conference 2001 Conference Paper

On optimal slicing of parallel programs

Markus Müller-Olm
Helmut Seidl

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.

Details