Methods for measuring pedestrian density, flow, speed and direction with minimal scatter (2009)
Steffen, Bernhard, Seyfried, Armin
The progress of image processing during recent years allows the measurement of pedestrian characteristics on a "microscopic" scale with low costs. However, density and flow are concepts of fluid...
Bio-jETI: a framework for semantics-based service composition (2009)
Lamprecht, Anna-Lena, Margaria, Tiziana, Steffen, Bernhard
Abstract Background The development of bioinformatics databases, algorithms, and tools throughout the last years has lead to a highly distributed world of bioinformatics services. Without adequate...
Proceedings 13 Volume Editors (2009)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Natural Language and
Semantic Web Services Challenge 2008 Synthesizing the Mediator with jABC/ABC (2009)
Tiziana Margaria, Marco Bakera, Harald Raffelt, Bernhard Steffen
Abstract. In this paper we show how to apply a tableau-based software composition technique to automatically generate the mediator’s service logic. This uses an LTL planning (or configuration)...
The Power of Assignment Motion Jens Knoop Universit"at Passau \Lambda (2009)
1 Motivation A major source for improving the run-time efficiency of a program is to avoid unnecessary recomputations and reexecutions of values (expressions) and instructions (assignments), as it is...
CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems (2009)
Issarny, Valérie, Steffen, Bernhard, Jonsson, Bengt, Blair, Gordon, Grace, Paul, Kwiatkowska, Marta, ...
The CONNECT European project that started in February 2009 aims at dropping the interoperability barrier faced by today's distributed systems. It does so by adopting a revolutionary approach to the...
CONNECT Challenges: Towards Emergent Connectors for Eternal Networked Systems (2009)
Issarny, Valérie, Steffen, Bernhard, Jonsson, Bengt, Blair, Gordon, Grace, Paul, Kwiatkowska, Marta, ...
The CONNECT European project that started in February 2009 aims at dropping the interoperability barrier faced by today's distributed systems. It does so by adopting a revolutionary approach to the...
MetaFrame in Practice: Design of Intelligent Network Services (2008)
Bernhard Steffen, Tiziana Margaria
Abstract. In this paper we present MetaFrame, an environment for formal methods-based, application-specific software design. Characteristic for MetaFrame are the following features: library-based...
Partial Dead Code Elimination Jens Knoop Universit"at Passau \Lambda (2008)
1 Motivation Dead code elimination is a technique for improving the efficiency of a program by avoiding the execution of unnecessary statements at run-time. Usually, an
Tiziana Margaria, Christian Kubczak, Bernhard Steffen
development of new technologies in proteomics, glycoanalysis, proteinbiochips, biostatistics and bioinformatics in terms of Life-Science (see the Website at www.zap-do.de). This project is...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
On the Evolution of Reactive Components- A Process-Algebraic Approach- (2008)
Bernhard Steffen, Rance Cleavel
1 Introduction Practical software development relies heavily on the use of libraries of previously implemented components. By allowing the cost of module development to be amortized over the number...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in any other way, and storage in data banks....
GeneFisher-P: variations of GeneFisher as processes in Bio-jETI (2008)
Lamprecht, Anna-Lena, Margaria, Tiziana, Steffen, Bernhard, Sczyrba, Alexander, Hartmeier, Sven, Giegerich, Robert
Abstract Background PCR primer design is an everyday, but not trivial task requiring state-of-the-art software. We describe the popular tool GeneFisher and explain its recent restructuring using...
Margaria, Tiziana, Kubczak, Christian, Steffen, Bernhard
Abstract Background With Bio-jETI, we introduce a service platform for interdisciplinary work on biological application domains and illustrate its use in a concrete application concerning statistical...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Solving the SWS-Challenge mediation problem with the jABC/jETI (2008)
Christian Winkler, Tiziana Margaria, Christian Kubczak, Bernhard Steffen, Stefan Naujokat
framework
Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Mohamed Hussein, Dekan Prof, Dr. Bernhard Steffen, Gutachter Prof, ...
In the classical scheduling problems, it has been assumed that complete knowledge of the problem was available when it was to be solved. However, scheduling problems in the real world face the...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Service-Oriented Design: The jABC Approach (2008)
Tiziana Margaria, Bernhard Steffen, Manfred Reitenspieß
Service-Oriented Design has driven the development of telecommunication infrastructure and applications, in particular the so-called Intelligent Network (IN) Services, since the early 90s: IN...
Comparing Heuristics for Model Based Testsuite Generation (2008)
Modellbasierte Entwicklung, Informatik Bericht, Tu Braunschweig, Jörg Desel, Matthias Gehrke, Petra Nawratil, ...
Michael von der Beek............................................................................................ 1 Einsatz von Modell-basierten Entwicklungstechniken in sicherheitsrelevanten...
jMosel: A Flexible Tool-Set for Monadic Second-Order Logic on Strings (2008)
Christian Topnik, Eva Wilhelm, Tiziana Margaria, Bernhard Steffen
Abstract. jMosel is a tool-set for the analysis and verification of linear parametric systems in monadic second-order logic on strings. In this paper we concentrate on the presentation of the core...
On the Evolution of Reactive Components – A Process-Algebraic Approach – (2008)
Markus Müller-olm, Bernhard Steffen, Rance Cleavel
Abstract. A common problem in library-based programming is the downward compatibility problem: will a program using an existing version of a library continue to function correctly with an upgraded...
Doktors Der Naturwissenschaften, Markus Kukuk, Prof Dr, Bernhard Steffen
Dedicated to my father Albert
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Full Life-Cycle Support for End-to-End Processes (2008)
Bernhard Steffen, Prakash Narayan, Sun Microsystems
Fully supporting end-to-end processes requires combining service orientation—which takes an engineering approach to reducing the gap between software requirements and implementation—with...
Relevance Feedback for Sketch Retrieval Based on Linear Programming Classification (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, ...
Abstract. Relevance feedback plays as an important role in sketch retrieval as it does in existing content-based retrieval. This paper presents a method of relevance feedback for sketch retrieval by...
Marco Bakera, Tiziana Margaria, Clemens D. Renner, Bernhard Steffen, Marco Bakera, Tiziana Margaria, ...
In this paper, we show how to use GEAR, a game-based model checker, for property-driven functional healing of high-assurance systems. Designers and engineers can interactively investigate the winning...
Christian Kubczak, Arno Fritsch, Tiziana Margaria, Bernhard Steffen
LC/MS is a successful analysis technique for the statistical analysis used in several branches of biology. It requires an intense screening and combination of the raw data, which is usually done with...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Commenced Publication in 1973 Founding and Former Series Editors: (2008)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Abstract Lazy Code Motion (2008)
Jens Knoop, Oliver Ruthing, Bernhard Steffen
We present a bit-vector algorithm for the optimal and economical placement of computations within flow graphs, which is as eficient as standard uni-directional analyses. The point of our algorithm is...
Anna-lena Lamprecht, Tiziana Margaria, Bernhard Steffen, Er Sczyrba, Robert Giegerich
on the development of new technologies in proteomics, glycoanalysis, proteinbiochips, biostatistics and bioinformatics in terms of Life-Science (see the Website at www.zap-do.de). PCR primer design...
The repulsive force in continous space models of pedestrian movement (2008)
Steffen, Bernhard, Seyfried, Armin
Pedestrian movements can be modeled at different degrees of detail. While flux models (Predeshensky/Milinski 1971) and cellular automata models (Schreckenberg 2002) give answers to some important...
Die Gaststudenten und ihre Betreuer waren: (2008)
Interner Bericht, Matthias Bolten (hrsg, Jülich Supercomputing Centre, Interner Bericht, Matthias Bolten (hrsg, ...
Entsprechend dem fächerübergreifenden Charakter des Wissenschaftlichen Rechnens waren Studenten der Natur- und Ingenieurwissenschaften, der Mathematik und Informatik angesprochen. Die Bewerber
GeneFisher-P: variations of GeneFisher as processes in Bio-jETI (2008)
Bmc Bioinformatics, Anna-lena Lamprecht, Tiziana Margaria, Bernhard Steffen, Er Sczyrba, Sven Hartmeier, ...
This article is available from:
Te Mathematik, Interner Bericht, Achim Basermann, Bernhard Steffen, A. Basermann, ...
INTRODUCTION The simulation of molecular dynamics and structural mechanics problems is a source of computationally challenging large sparse eigenvalue problems. To solve such problems, we develop...
Modal Transition Systems (2007)
Kim G. Larsen, Kim G. Larsen, Bernhard Steffen, Bernhard Steffen, Carsten Weise, Carsten Weise
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
Oliver Niese, Tiziana Margaria, Andreas Hagerer, Bernhard Steffen, Georg Brune, Werner Goerigk, ...
In this paper we present an integrated testing environment for the automated regression test of Computer Telephony Integrated applications. Its novelty consists of a coordinative test management...
Andreas Hagerer, Tiziana Margaria, Oliver Niese, Bernhard Steffen, Georg Brune, Hans-dieter Ide
Abstract. In this paper we show how the workfllow-oriented, library-based test design and execution environment presented in [8] fulfills the promise of enabling efficient integrated system-level...
Oliver Niese, Tiziana Margaria, Andreas Hagerer, Markus Nagelmann, Bernhard Steffen, Georg Brune, ...
Abstract. In this paper we present an automated testing environment for the system level test of Computer Telephony Integrated applications. Its novelty consists of a coordinative test management...
Alfons Geser, Jens Knoop, Gerald Luttgen, Oliver Ruthing, Bernhard Steffen
Abstract. We present a new fixpoint theorem which guarantees the existence and the finite computability of the least common solution of a countable system of recursive equations over a wellfounded...
System Level Testing of Virtual Switch (Re)Configuration over IP (2007)
Tiziana Margaria, Metaframe Technologies Gmbh, Oliver Niese, Bernhard Steffen, Andrei Erochok
We show how our integrated test environment can be used for the validation of evolving internet services, since it captures the (re-)configuration phase preceding the `classical ' steady state...
Tiziana Margaria, Oliver Niese, Bernhard Steffen
Abstract. Modern IP-based applications are multitiered, distributed applications that typically run on heterogeneous platforms. Their correct operation depends increasingly on the interoperability of...
Verification on Infinite Structures Olaf Burkart (2007)
Didier Caucal, Faron Moller, Bernhard Steffen, Lehrstuhl Informatik V, Lehrstuhl Informatik V
Abstract. In this chapter, we present a hierarchy of infinite-state systems based on the primitive operations of sequential and parallel composition; the hierarchy includes a variety of...
Tiziana Margaria, Bernhard Steffen, W. Rance Cleavel
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
A Formal Requirements Engineering Method for Specification, Synthesis, and Verification (2007)
Tiziana Margaria, Bernhard Steffen
This paper presents a formal requirements engineering method capturing specification, synthesis, and verification. Being multi-paradigm, our approach integrates individual established formal methods:...
A Practical Approach for the Regression Testing (2007)
Tiziana Margaria, Oliver Niese, Bernhard Steffen
Modern IP-based applications are multitiered, distributed applications that typically run on heterogeneous platforms. Their correct operation depends increasingly on the interoperability of single...
Test and Testing Control Platform (TTCP) (2007)
Steffen, Bernhard, Rüthing, Oliver, Raffelt, Harald, Deiß, Thomas, Altinata, Adem, Carrillo De Albornoz, Jorge, ...
New insights into pedestrian flow through bottlenecks (2007)
Seyfried, Armin, Rupprecht, Tobias, Passon, Oliver, Steffen, Bernhard, Klingsch, Wolfram, Boltes, Maik
Capacity estimation is an important tool for the design and dimensioning of pedestrian facilities. The literature contains different procedures and specifications which show considerable differences...
des John von Neumann-Instituts für Computing (2007)
Jülich Supercomputing Centre, Interner Bericht, Matthias Bolten (hrsg, Eduardo Aguilar, Moreno Bernd Körfgen, Sebastian Birk, ...
Computing (NIC) und hiermit des JSC als wesentlicher Säule des NIC. Um den akademischen Nachwuchs mit verschiedenen Aspekten des Wissenschaftlichen Rechnens vertraut zu machen, führte das JSC in...
des John von Neumann-Instituts für Computing (2007)
Jülich Supercomputing Centre, Interner Bericht, Matthias Bolten (hrsg, Eduardo Aguilar, Moreno Bernd Körfgen, Sebastian Birk, ...
Computing (NIC) und hiermit des JSC als wesentlicher Säule des NIC. Um den akademischen Nachwuchs mit verschiedenen Aspekten des Wissenschaftlichen Rechnens vertraut zu machen, führte das JSC in...
Die Gaststudenten und ihre Betreuer waren: (2006)
Forschungszentrum Jülich Gmbh, Interner Bericht, Rüdiger Esser (hrsg, Mathias Aust, Guido Arnold, Marcus Richter, ...
Computing (NIC) und hiermit des ZAM als wesentlicher Säule des NIC. Um den akademischen Nachwuchs
Learning Interpretable Models (2006)
Dissertation Zur Erlangung, Doktors Der Naturwissenschaften, Stefan Rüping, Dekan Prof, Dr. Bernhard Steffen, ...
Contents 1 Introduction 11 1.1 Interpretability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.1.1 Interpretability as Part of the Data Mining Process . . . . 13 1.1.2 Interpretability...
B: Modelbased Design of Distributed Collaborative Bioinformatics Processes in the jABC (2006)
Tiziana Margaria, Christian Kubczak, Mark Njoku, Bernhard Steffen
Abstract — Our approach to the model-driven collaborative design of workflows for bioinformatic applications uses the jABC [6] for model driven mediation and choreography to complement a...
Commenced Publication in 1973 Founding and Former Series Editors: (2006)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Pilar Herrero et al. (Eds.) On the Move to Meaningful Internet Systems 2006:
Service-Oriented Design: The jABC Approach (2006)
Margaria, Tiziana, Steffen, Bernhard, Reitenspieß, Manfred
Reviewing our 10 years of experience in service engineering for telecommunication systems from the point of view of Service-Oriented Design then and now, we observe that much is common to the two...
Basics of Modelling the Pedestrian Flow (2005)
Seyfried, Armin, Steffen, Bernhard, Lippert, Thomas
For the modelling of pedestrian dynamics we treat persons as self-driven objects moving in a continuous space. On the basis of a modified social force model we qualitatively analyze the influence of...
The Fundamental Diagram of Pedestrian Movement Revisited (2005)
Seyfried, Armin, Steffen, Bernhard, Klingsch, Wolfram, Boltes, Maik
The empirical relation between density and velocity of pedestrian movement is not completely analyzed, particularly with regard to the `microscopic' causes which determine the relation at medium and...
The Fundamental Diagram of Pedestrian Movement Revisited (2005)
Armin Seyfried, Bernhard Steffen, Wolfram Klingsch, Maik Boltes
The empirical relation between density and velocity of pedestrian movement is not completely analyzed, particularly with regard to the ‘microscopic ’ causes which determine the relation at medium...
Die Gaststudenten und ihre Betreuer waren: (2005)
Forschungszentrum Jülich Gmbh, Interner Bericht, Rüdiger Esser (hrsg, Claudia Albrecht, Wolfgang Meyer, Quang Minh, ...
Computing (NIC) und hiermit des ZAM als wesentlicher Säule des NIC. Um den akademischen Nachwuchs
On the correspondence between conformance testing and regular inference (2005)
Therese Berg, Olga Grinchtein, Bengt Jonsson, Martin Leucker, Harald Raffelt, Bernhard Steffen
Abstract. Conformance testing for finite state machines and regular inference both aim at identifying the model structure underlying a black box system on the basis of a limited set of observations....
Die Gaststudenten und ihre Betreuer waren: (2005)
Forschungszentrum Jülich Gmbh, Interner Bericht, Rüdiger Esser (hrsg, Claudia Albrecht, Wolfgang Meyer, Quang Minh, ...
Computing (NIC) und hiermit des ZAM als wesentlicher Säule des NIC. Um den akademischen Nachwuchs
On the correspondence between conformance testing and regular inference (2005)
Therese Berg, Olga Grinchtein, Bengt Jonsson, Martin Leucker, Harald Raffelt, Bernhard Steffen
Abstract. Conformance testing for finite state machines and regular inference both aim at identifying the model structure underlying a black box system on the basis of a limited set of observations....
Dekan Dekanin, Prof Dr, Bernhard Steffen, Gutachter Prof, ...
1.1 Computer experiments............................ 10 1.2 Objectives of this work............................ 12
A Complete Method for the Synthesis of Linear Ranking Functions (2004)
Podelski, Andreas, Rybalchenko, Andrey, Levi, Giorgio, Steffen, Bernhard
des John von Neumann-Instituts für Computing (2004)
Forschungszentrum Jülich Gmbh, Interner Bericht, Rüdiger Esser (hrsg, Nikos Elpidoforou, Paul Gibbon, Ivo Kabadshow, ...
Computing (NIC) und hiermit des ZAM als wesentlicher Säule des NIC. Um den akademischen Nachwuchs
A Complete Method for the Synthesis of Linear Ranking Functions (2004)
Podelski, Andreas, Rybalchenko, Andrey, Levi, Giorgio, Steffen, Bernhard
Test-Based Model Generation for Legacy Systems (2003)
Hardi Hungar, Tiziana Margaria, Bernhard Steffen
We study the extension of applicability of system-level testing techniques to the construction of a consistent model of (legacy) systems under test, which are seen as black boxes. We gather...
des John von Neumann-Instituts für Computing (2003)
Forschungszentrum Jülich Gmbh, Interner Bericht, Rüdiger Esser (hrsg, Matthias Bolten, Thomas Müller, Björn Hagemeier, ...
Computing (NIC) und hiermit des ZAM als wesentlicher Säule des NIC. Um den akademischen Nachwuchs
des John von Neumann-Instituts für Computing (2003)
Forschungszentrum Jülich Gmbh, Interner Bericht, Rüdiger Esser (hrsg, Matthias Bolten, Thomas Müller, Björn Hagemeier, ...
Computing (NIC) und hiermit des ZAM als wesentlicher Säule des NIC. Um den akademischen Nachwuchs
Subspace methods for sparse eigenvalue problems published in
Bernhard Steffen, Bernhard Steffen, John Neumann
Subspace methods are the methods of choice for calculating a few eigenvalues and-vectors of a large matrix. They may also be considered for completely diagonalizing a matrix if it is either very...
Bernhard Steffen, B. Steffen, John Neumann
The problem of calculating some or all eigenvalues and-vectors of a large matrixappears in a wide range of applications from biology (meta stable states of ecosystems) to mechanical engineering...
Bernhard Steffen, Second Edition, J. Grotendorst (ed, Bernhard Steffen
Permission to make digital or hard copies of portions of this work for personal or classroom use is granted provided that the copies are not made or distributed for profit or commercial advantage and...
Expansion-based Removal of Semantic Partial Redundancies (1999)
Jens Knoop, Oliver Rüthing, Bernhard Steffen
We develop an expansion-based algorithm for semantic partial redundancy elimination (SPRE), which overcomes the central drawbacks of the state-of-the-art approaches, which leave the program structure...
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Proceedings
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Proceedings
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Proceedings
Program analysis as model checking of abstract interpretations (1998)
David Schmidt, Bernhard Steffen
Abstract. This paper presents a collection of techniques, a methodology, in which abstract interpretation, flow analysis, and model checking are employed in the representation, abstraction, and...
Program analysis as model checking of abstract interpretations (1998)
David Schmidt, Bernhard Steffen
Abstract. This paper presents a collection of techniques, a methodology, in which abstract interpretation, flow analysis, and model checking are employed in the representation, abstraction, and...
Backtracking-free design planning by automatic synthesis in metaframe (1998)
Tiziana Margaria, Bernhard Steffen
Abstract. We present an environment supporting the flexible and application-specific construction of design plans, which avoids the insurgence of unsuccessful design plans at design time, and is thus...
Program Analysis as Model Checking of Abstract Interpretations (1998)
David Schmidt, Bernhard Steffen
Interpretations David Schmidt Bernhard Ste#en Kansas State University # (USA) Universitat Dortmund ## (D) Abstract. This paper presents a collection of techniques, a methodology, in which abstract...
Code Motion and Code Placement: Just Synonyms? (1998)
Jens Knoop, Oliver Rüthing, Bernhard Steffen
We prove that there is no difference between code motion (CM ) and code placement (CP) in the traditional syntactic setting, however, a dramatic difference in the semantic setting. We demonstrate...
Program analysis as model checking of abstract interpretations (1998)
David Schmidt, Bernhard Steffen
Abstract. This paper presents a collection of techniques, a methodology, in which abstract interpretation, flow analysis, and model checking are employed in the representation, abstraction, and...
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
Femke van Raamsdonk Roel de Vrijer (Eds.)
Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Editorial Board, David Hutchison, Takeo Kanade, ...
concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in any other way, and storage in data banks....
Model checking the full modal mu-calculus for infinite sequential processes (1997)
Olaf Burkart, Bernhard Steffen
Infinite-state systems, context-free processes, pushdown processes, regular graphs, modal mu-calculus, model-checking. In this paper we develop a new elementary algorithm for model-checking infinite...
Bernhard Steffen, Tiziana Margaria, Michael Beeck, Lehrstuhl Fur Programmiersysteme
We present PM-MetaFrame, a tool for automatic synthesis (i.e. prior to any enaction) of linear process models from specifications written as global constraints in linear time temporal logic. Key to...
Basic-block Graphs: Living Dinosaurs? (1997)
Jens Knoop, Dirk Koschützki, Bernhard Steffen
Since decades, basic-block (BB) graphs are the state-of-the-art means for representing programs in advanced industrial compiler environments. The usual justification for introducing the intermediate...
Code Motion and Code Placement: Just Synonyms? (1997)
Just Synonyms, Jens Knoop, Oliver Rüthing, Bernhard Steffen
We prove that there is no difference between code motion (CM ) and code placement (CP) in the traditional syntactic setting, however, a dramatic difference in the semantic setting. We demonstrate...
Forschungszentrum J, Ulich Gmbh, Interner Bericht, Achim Basermann, Achim Basermann, Bernhard Steffen, ...
We present preconditioned solvers to find a few eigenvalues and eigenvectors of large dense or sparse symmetric matrices based on the Jacobi-Davidson (JD) method by G. L. G. Sleijpen and H. A. van...
Graphs in METAFrame: The Unifying Power of Polymorphism (1997)
Volker Braun, Andreas Claßen, V. Braun, Carsten Friedrich, Achim Dannecker, ...
. We present a highly polymorphic tool for the construction, synthesis, structuring, manipulation, investigation, and (symbolic) execution of graphs. The flexibility of this tool, which mainly arises...
Compositional Minimisation of Finite State Systems Using Interface Specifications (1996)
Susanne Graf, Bernhard Steffen, Gerald Lüttgen
We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused...
Compositional Minimisation of Finite State Systems Using Interface Specifications (1996)
Susanne Graf, Bernhard Steffen, Gerald Lüttgen
. We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused...
Non-monotone Fixpoint Iterations to Resolve Second Order Effects (1996)
Alfons Geser, Jens Knoop, Gerald Lüttgen, Oliver Rüthing, Bernhard Steffen, Bernhard Ste En
We present a new fixpoint theorem which guarantees the existence and the finite computability of the least common solution of a countable system of recursive equations over a wellfounded domain. The...
Compositional Minimisation of Finite State Systems Using Interface Specifications (1996)
Speci Cations, Bernhard Steffen, Susanne Graf, Bernhard Ste En, Gerald Lüttgen
We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused...
Non-monotone Fixpoint Iterations to Resolve Second Order Effects (1996)
Alfons Geser, Jens Knoop, Gerald Lüttgen, Oliver Rüthing, Bernhard Steffen, Passau Germany
We present a new fixpoint theorem which guarantees the existence and the finite computability of the least common solution of a countable system of recursive equations over a wellfounded domain. The...
The METAFrame'95 Environment (1996)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun
programs whose implementation is supported by the automatic, library-based synthesis of linear compositions of modules. More complex control structures glueing the linear portions together must be...
Heterogeneous Analysis and Verification for Distributed Systems (1996)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Lehrstuhl Fur Informatik
In this paper we present an environment for the development of special purpose heterogeneous analysis and verification tools, which is unique in 1) constituting a framework for the development of...
Incremental Formalization: a Key to Industrial Success (1996)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun, Lehrstuhl Fur Programmiersysteme
views focus the development process, and support error correction. This approach provides an incremental use of formal methods: if no formal constraints are defined, our system behaves like standard...
The Methodology of Modal Constraints (1996)
Kim G. Larsen, Bernhard Steffen, Carsten Weise
. We present a complete solution of the RPC-Memory Specification Problem, by applying a constraint-oriented state-based proof methodology for concurrent software systems. Our methodolgy exploits...
Parallelism for Free: Efficient and Optimal Bitvector Analyses for Parallel Programs (1996)
Jens Knoop, Bernhard Steffen, Jürgen Vollmer, J Urgen Vollmer
ing with credit is permitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any component of this work in other works, requires prior specific permission...
Parallelism for Free: Efficient and Optimal Bitvector Analyses for Parallel Programs (1996)
Jens Knoop, Bernhard Steffen, Jurgen Vollmer
In this paper we show how to construct optimal bitvector analysis algorithms for parallel programs with shared memory that are as efficient as their purely sequential counterparts, and which can...
Non-monotone Fixpoint Iterations to Resolve Second Order Effects (1996)
Alfons Geser, Jens Knoop, Gerald Lüttgen, Oliver Rüthing, Bernhard Steffen
. We present a new fixpoint theorem which guarantees the existence and the finite computability of the least common solution of a countable system of recursive equations over a wellfounded domain....
Service Creation: Formal Verification and Abstract Views (1996)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun, Manfred Reitenspie, Helmut Wendler, ...
Views Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun Universitat Passau (Germany) Manfred Reitenspieß, Helmut Wendler SiemensNixdorf Informationssysteme AG y , Munich (Germany)...
Compositional Minimisation of Finite State Systems Using Interface Specifications (1996)
Susanne Graf, Bernhard Steffen, Gerald Lüttgern
Semantics) For a 2 A consider the functions E I a : 2 L(I) ! 2 L(I) with E I a (L) = df ae L a if a 2 A I L otherwise Then the local abstract semantic functions for (q; a; q 0 ) 2\Gamma! p with...
Incremental Formalization (1996)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun
views focus the development process, and support error correction. This approach provides an incremental use of formal methods: if no formal constraints are defined, our system behaves like standard...
A Constraint-Oriented Service Creation Environment (1996)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun, Viola Kriete, Manfred Reitenspieß, ...
ion Concretization Modification Control Control Service Libraries Selection Figure 1: The Service Creation Process ffl The service provider is familiar with the specific customer needs and enters...
Automatic Synthesis of Design Plans in MetaFrame (1996)
In Metaframe, Tiziana Margaria, Bernhard Steffen, Lehrstuhl Fur Programmiersysteme
We present CAD-MetaFrame, an environment supporting the flexible CAD tool integration and application-specific construction of design plans, which avoids the insurgence of unsuccessful design plans...
An Environment for the Creation of Intelligent Network Services (1996)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun, Lehrstuhl Fur Programmiersysteme, Manfred Reitenspie
This paper presents a Service Creation Environment which is unique in offering global correctness and consistency checks. These guarantee frame conditions for the design concerning implementability,...
Towards a Tool Kit for the Automatic Generation of Interprocedural Data Flow Analyses (1996)
Jens Knoop, Oliver Rüthing, Oliver R, Bernhard Steffen
this article, the classical application of DFA. In this context, designers of a DFA are typically faced with the problem of how to construct an algorithm that determines the set of program points of...
A Constraint-Oriented Service Creation Environment (1996)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun, Manfred Reitenspieß, Siemens Nixdorf, ...
The challenge of this joint project was to design and implement an environment for the creation of advanced telephone services (Intelligent Network Services) on the basis of a library of basic...
Fischer's Protocol Revisited: A Simple Proof Using Modal Constraints (1996)
Kim G. Larsen, Bernhard Steffen, Carsten Weise
. As a case study, we apply a constraint-oriented state-based proof methodology to Fischer's protocol. The method exploits compositionality and abstraction to reduce the investigated...
Parallelism for free: Efficient and optimal bitvector analyses for parallel programs (1996)
Jens Knoop, Bernhard Steffen, Jürgen Vollmer
We consider parallel programs with shared memory and interleaving semantics, for which we show how to construct for unidirectional bitvector problems optimal analysis algorithms that are as efficient...
A constraint oriented proof methodology based on modal transition systems (1995)
Kim G. Larsen, Bernhard Steffen, Carsten Weise
In this paper, we present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification...
Compositional Minimization of Finite State Systems Using Interface Specifications (1995)
Susanne Graf, Bernhard Steffen, Bernhard Ste En, Gerald Lüttgen
In this paper we present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state...
A Constraint Oriented Proof Methodology Based on Modal Transition Systems (1995)
Kim G. Larsen, Bernhard Steffen, Carsten Weise
We present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under...
Heterogeneous Analysis and Verification for Distributed Systems (1995)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Lehrstuhl Fur Informatik
In this paper we present an environment for the development of special purpose heterogeneous analysis and verification tools, which is unique in 1) constituting a framework for the development of...
Optimal Code Motion for Parallel Programs (1995)
Jens Knoop, Bernhard Steffen, Jürgen Vollmer
Code motion is well-known as a powerful technique for the optimization of sequential programs. It improves the run-time efficiency by avoiding unnecessary recomputations of values, and it is even...
Incremental Formalization: a Key to Industrial Success (1995)
Bernhard Steffen, Tiziana Margaria, Andreas Claßen, Volker Braun, Lehrstuhl Fur Programmiersysteme
Views . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 9.2 Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 10 Conclusions, Experience and...
An Approach to Intelligent Software Library Management (1995)
Burkhard Freitag, Bernhard Steffen, Tiziana Margaria, Ulrich Zukowski
Although very important, solely supporting the retrieval of single components from a software library is not enough to make efforts towards software reuse a success. The DaCapo software library...
Compositional Minimisation of Finite State Systems Using Interface Specifications (1995)
Susanne Graf, Bernhard Steffen, Gerald Lüttgen
In this paper we present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state...
Optimal Code Motion for Parallel Programs (Extended Abstract) (1995)
Jens Knoop, Bernhard Steffen, Jürgen Vollmer
Jens Knoop y Bernhard Steffen y Jurgen Vollmer z Keywords: Parallelism, interleaving semantics, synchronization, compiler, program optimization, data flow analysis, bitvector problems, code motion,...
Tools and Algorithms for the Construction and Analysis of Systems (1995)
Uffe H. Engberg, Kim G. Larsen, Arne Skou (Eds.), Arne Skou (editors, Jens Knoop, Bernhard Steffen, ...
In this paper we show how to construct optimal bitvector analysis algorithms for parallel programs with shared memory that are as efficient as their purely sequential counterparts, and which can...
Priority as Extremal Probability (1995)
Scott A. Smolka, Bernhard Steffen
We extend the stratified model of probabilistic processes presented in [vGSS] to obtain a very general notion of process priority . The main idea is to allow probability guards of value 0 to be...
The Fixpoint-Analysis Machine (1995)
Bernhard Steffen, Andreas Claßen, Marion Klein, Jens Knoop, Tiziana Margaria
. We present a fixpoint-analysis machine, for the efficient computation of homogeneous, hierarchical, and alternating fixpoints over regular, context-free/push-down and macro models. Applications of...
Optimal Code Motion for Parallel Programs (1995)
Jens Knoop, Bernhard Steffen, Jürgen Vollmer
Code motion is well-known as a powerful technique for the optimization of sequential programs. It improves the run-time efficiency by avoiding unnecessary recomputations of values, and it is even...
An Environment for the Creation of Intelligent Network Services (1995)
Bernhard Steffen, Tiziana Margaria, Volker Braun, Manfred Reitenspie, Siemens Nixdorf, Informationssysteme Ag
This paper presents a Service Creation Environment which is unique in offering global correctness and consistency checks. These guarantee frame conditions for the design concerning implementability,...
The Power of Assignment Motion (1995)
Jens Knoop, Oliver Rüthing, Bernhard Steffen
Assignment motion (AM) and expression motion (EM) are the basis of powerful and at the first sight incomparable techniques for removing partially redundant code from a program. Whereas AM aims at the...
A Constraint Oriented Proof Methodology based on Modal Transition Systems (1995)
Kim G. Larsen, Bernhard Steffen, Carsten Weise
We present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under...
A constraint oriented proof methodology based on modal transition systems (1995)
Kim G. Larsen, Kim G. Larsen, Carsten Weise, Carsten Weise, Bernhard Steffen, Bernhard Steffen
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent...
Chaotic Fixed Point Iterations (1994)
Alfons Geser, Jens Knoop, Gerald Lüttgen, Bernhard Steffen, Oliver Rüthing
In this paper we present a new fixed point theorem applicable for a countable system of recursive equations over a wellfounded domain. Wellfoundedness is an essential feature of many computer science...
Chaotic Fixed Point Iterations (1994)
Alfons Geser, Jens Knoop, Gerald Lüttgen, Bernhard Steffen, Bernhard Ste En, ...
In this paper we present a new fixed point theorem applicable for a countable system of recursive equations over a wellfounded domain. Wellfoundedness is an essential feature of many computer science...
Parallelism for Free: Efficient and Optimal Bitvector Analyses for Parallel Programs (1994)
Jens Knoop, Bernhard Steffen, Jürgen Vollmer
In this paper we show how to construct optimal bitvector analysis algorithms for parallel programs with shared memory that are as efficient as their purely sequential counterparts, and which can...
The Concurrency Workbench: A Semantics Based Tool for the Verification of Concurrent Systems (1994)
Rance Cleaveland, Joachim Parrow, Bernhard Steffen
The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth: a variety...
Finite Model Checking and Beyond (1994)
This paper reviews finite and infinite-state model checking form two pragmatic perspectives: the application to the static analysis of imperative programs or data flow analysis, and the...
A Pragmatic Approach to Software Synthesis (1994)
Burkhard Freitag Tiziana, Tiziana Margaria, Bernhard Steffen
We present a practice oriented tool for software synthesis that supports the interface -correct configuration of complex systems from a library of reusable software components. Besides simply...
Partial Dead Code Elimination (1994)
Jens Knoop, Oliver Rüthing, Bernhard Steffen
A new aggressive algorithm for the elimination of partially dead code is presented, i.e., of code which is only dead on some program paths. Besides being more powerful than the usual approaches to...
Chaotic Fixed Point Iterations (1994)
Alfons Geser, Jens Knoop, Gerald Lüttgen, Bernhard Steffen, Oliver Ruthing
In this paper we present a new fixed point theorem applicable for a countable system of recursive equations. We demonstrate the power and versatility of our result by applications in automata theory...
Parallelism for Free: Efficient and Optimal Bitvector Analyses for Parallel Programs (1994)
Jens Knoop, Bernhard Steffen, Jürgen Vollmer
In this paper we show how to construct optimal bitvector analysis algorithms for parallel programs with shared memory that are as efficient as their purely sequential counterparts, and which can...
Deductive Database Support for Software Configuration (1994)
Burkhard Freitag, Tiziana Margaria, Bernhard Steffen
We show that deductive database techniques can successfully used to support the interface-correct configuration of complex systems from a library of reusable software components. Besides simply...
A Pragmatic Approach to Software Synthesis (1994)
Burkhard Freitag, Tiziana Margaria, Bernhard Steffen
We present a practice oriented tool for software synthesis that supports the interface -correct configuration of complex systems from a library of reusable software components. Besides simply...
Optimal Code Motion: Theory and Practice (1994)
Jens Knoop, Oliver Rüthing, Oliver R, Bernhard Steffen
this paper, we emphasize the practicality of lazy code motion by giving explicit directions for its implementation in standard compiler environments. In particular, we present a version of the...
An Elementary Bisimulation Decision Procedure for Arbitrary Context-Free Processes (1994)
Olaf Burkart, Didier Caucal, Bernhard Steffen, Aachener Informatikbericht
We present an elementary algorithm for deciding bisimulation equivalence between arbitrary context-free processes. This improves on the state of the art algorithm of Christensen, Huttel and Stirling...
Niedermann. Automatic Synthesis of Real Time Systems. December (1994)
Jens Chr Godskesen, Kim G. Larsen, Bernhard Steffen, Carsten Weise, A Constraint, ...
[RS-94-44] Abstract, PostScript.
Module Configuration by Minimal Model Construction (1993)
Bernhard Steffen, Tiziana Margaria, Burkhard Freitag
We present a framework for the automatic configuration of large systems from a library of reusable software components. Core of the framework is a modal logic that uniformly and elegantly captures...
A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus (1993)
Rance Cleaveland, Bernhard Steffen
We develop a model-checking algorithm for a logic that permits propositions to be defined using greatest and least fixed points of mutually recursive systems of equations. This logic is as expressive...
Distinguishing Formulas for Free (1993)
Tiziana Margaria, Bernhard Steffen, Aachener Informatikberichte
A system for the efficient verification of the input/output correctness of Finite State Machines with data path and control unit is presented. This system, which is based on FirstOrder Logic theorem...
Optimal Code Motion: Theory and Practice (1993)
Jens Knoop, Oliver Rüthing, Bernhard Steffen
An implementation oriented algorithm for lazy code motion is presented that minimizes the number of computations in programs while suppressing any unnecessary code motion in order to avoid...
Module Configuration by Minimal Model Construction (1993)
Bernhard Steffen, Tiziana Margaria, Lehrstuhl Fur Informatik, Burkhard Freitag
We present a framework for the automatic configuration of large systems from a library of reusable software components. Core of the framework is a modal logic that uniformly and elegantly captures...
Generating Data Flow Analysis Algorithms from Modal Specifications (1993)
The paper develops a framework that is based on the idea that modal logic provides an appropriate framework for the specification of data flow analysis (DFA) algorithms as soon as programs are...
Lazy Strength Reduction (1993)
Jens Knoop, Oliver Rüthing, Bernhard Steffen
We present a bit-vector algorithm that uniformly combines code motion and strength reduction, avoids superfluous register pressure due to unnecessary code motion, and is as efficient as standard...
Pushdown Processes: Parallel Composition and Model Checking (1993)
Olaf Burkart, Bernhard Steffen
In this paper we consider a strict generalization of context-free processes, the pushdown processes, and show that this class of processes is 1) closed under parallel composition with finite state...
Jens Knoop, Oliver Ruthing, Bernhard Steffen, Rwth Aachen
We present a bit-vector algorithm for the optimal and economical placement of computations within flow graphs, which is as efficient as standard uni-directional analyses. The point of our algorithm...
Model Checking for Context-Free Processes (1992)
Olaf Burkart, Bernhard Steffen
We develop a model-checking algorithm that decides for a given context-free process whether it satisfies a property written in the alternation-free modal mucalculus. The central idea behind this...
The Interprocedural Coincidence Theorem (1992)
We present an interprocedural generalization of the well-known (intraprocedural) Coincidence Theorem of Kam and Ullman, which provides a sufficient condition for the equivalence of the meet over all...
Bericht Nr, Jens Knoop, Jens Knoop, Oliver Rüthing, Oliver Ruthing, Bernhard Steffen, ...
We present a bit-vector algorithm for the optimal and economical placement of computations within flow graphs, which is as efficient as standard uni-directional analyses. The point of our algorithm...
Computing Behavioural Relations, Logically (1991)
Rance Cleaveland, Bernhard Steffen
This paper develops a model-checking algorithm for a fragment of the modal mu-calculus and shows how it may be applied to the efficient computation of behavioral relations between processes. The...
Optimal Code Motion within Flow Graphs: A Practical Approach (1991)
Bernhard Steffen, Jens Knoop, ...
Common subexpression elimination, partial redundancy elimination and loop invariant code motion are all instances of the same general run-time optimization problem: how to optimally place...
Efficient Code Motion and an Adaption to Strength Reduction (1991)
Bernhard Steffen, Jens Knoop, Oliver Rüthing
this paper we consider two elaborations of this algorithm, which are dealt with in Part I and Part II, respectively. Part I deals with the problem that the full variant of the algorithm of [SKR1] may...
The concurrency workbench: A semantics based tool for the verification of concurrent systems (1991)
Rance Cleaveland, Joachim Parrow, Bernhard Steffen
Abstract The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth:...
Compositional minimization of finite state systems (1990)
Susanne Graf, Bernhard Steffen, Aachener Informatikberichte
In this paper we develop a compositional method for the construction of the minimal transition system that represents the semantics of a given reactive system. The point of this method is that it...
Reactive, Generative and Stratified Models of Probabilistic Processes (1990)
Scott A. Smolka, Bernhard Steffen
ion Let E; E 0 be PCCS expressions. The inter-model abstraction rule IMARGR is defined by E ff[p] \Gamma\Gamma! i E 0 =) E ff[p= G (E;fffg)] ae \Gamma\Gamma\Gamma\Gamma\Gamma\Gamma! i E 0 This rule...
Priority as Extremal Probability (1990)
Scott Smolka, Bernhard Steffen, Aachener Informatikberichte
We extend the stratified model of probabilistic processes presented in [vGSST90] to obtain a very general notion of process priority . The main idea is to allow probability guards of value 0 to be...
The Value Flow Graph: A Program Representation for Optimal Program Transformations (1990)
Bernhard Steffen, Jens Knoop, Oliver Rüthing
Data flow analysis algorithms for imperative programming languages can be split into two groups: first, into the semantic algorithms that determine semantic equivalence between terms, and second,...
Priority as Extremal Probability (1990)
Scott A. Smolka, Bernhard Steffen
We extend the stratified model of probabilistic processes presented in [vGSST90] to obtain a very general notion of process priority . The main idea is to allow probability guards of value 0 to be...
Mikroreprod. e. Ms. 183 Bl.
Zugl.: Kiel, Univ., Diss.
Die rechtliche Stellung der Gewerkschaft im gesellschaftlichen Gefüge des modernen Staates. (1953)
Kiel, Rechts- u. staatswiss. F., Diss. v. 2. April 1953 (Nicht f. d. Aust.).
GeneFisher-P: variations of GeneFisher as processes in Bio-jETI
Lamprecht, Anna-Lena, Margaria, Tiziana, Steffen, Bernhard, Sczyrba, Alexander, Hartmeier, Sven, Giegerich, Robert
Constraint-Based Inter-Procedural Analysis of Parallel Programs
Helmut Seidl, Bernhard Steffen
We provide a uniform framework for the analysis of programs with procedures and explicit, unbounded, fork/join parallelism covering not only bitvector problems like reaching definitions or live...
Jens Knoop, Oliver Ruthing, Bernhard Steffen
We present a bit-vector algorithm that uniformly combines code motion and strength reduction, avoids superfluous register pressure due to unnecessary code motion, and is as efficient as standard...
Compositional Characterization of Observable Program Properties
Bernhard Steffen, C. Barry Jay, Michael Mendler
In this paper we model both program behaviours and abstractions between them as lax functors, which generalize abstract interpretations by exploiting the natural ordering of program properties. This...