Bernhard Steffen (computer scientist)

Last updated

Bernhard Steffen (born 31 May 1958 in Kiel, West Germany) is a German computer scientist and professor at the TU Dortmund University, Germany. His research focuses on various facets of formal methods ranging from program analysis and verification, to workflow synthesis, to test-based modeling, and machine learning. [1]

Contents

After his PhD at the University of Kiel he spent two years as a research fellow at the LFCS (Edinburgh, Scotland) where he co-developed the Edinburgh Concurrency Workbench [2] and authored one of the earliest papers on how to adequately model probabilistic processes, [3] before joining the University of Aarhus in 1989 as a postdoc. From 1990 to 1992 he was associate professor at the RWTH Aachen, before he became full professor at the University of Passau. Since 1997 he holds the chair of programming systems at TU Dortmund University where he was Dean of Computer Science between 2002 and 2006 as well as a member of the Senate in 2006 and 2007. [1] In Dortmund he developed the concept of active automata learning to towards a practical means for model-based testing that does not require any a priori models. Recently his interest shifted towards the application of formal methods for explaining machine learning.

His conceptual background comprises abstract interpretation, computer-aided verification and explanation, automata learning, and the development of domain-specific languages that guarantee properties by design. This is witnessed by receiving the Most Influential PLDI Paper Award for Lazy Code Motion, which is given 10 years in retrospective, and the CAV Artifact Award for the Open-Source LearnLib. Finally, in 2019 he was awarded the title of Honorary Professor of the AMITY School of Engineering and Technology.

Furthermore, Steffen is founding Editor in Chief of STTT, [4] Co-Founder of TACAS, [5] ETAPS, [6] ISoLA, [7] RERS [8] and member of the editorial board of LNCS. [9]

Journal and conference foundations

Bernhard Steffen co-founded the following journals and conferences

Related Research Articles

In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

<span class="mw-page-title-main">Theoretical computer science</span> Subfield of computer science and mathematics

Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory.

Anatoly Abramovich Shalyto is a Russian scientist, doctor of sciences, and professor. He was awarded by Russian State Government in 2008 for his achievements in education and his development of the technology for Automata-based programming called "Switch-technology." He is also an initiator of the Open Project Documentation Initiative.

<span class="mw-page-title-main">Rajeev Alur</span> American computer scientist

Rajeev Alur is an American professor of computer science at the University of Pennsylvania who has made contributions to formal methods, programming languages, and automata theory, including notably the introduction of timed automata and nested words.

PRISM is a probabilistic model checker, a formal verification software tool for the modelling and analysis of systems that exhibit probabilistic behaviour. One source of such systems is the use of randomization, for example in communication protocols like Bluetooth and FireWire, or in security protocols such as Crowds and Onion routing. Stochastic behaviour also arises in many other computer systems, for example due to equipment failures or unpredictable communication delays. Yet another class of systems amenable to this kind of analysis are biochemical reaction networks.

<span class="mw-page-title-main">Construction and Analysis of Distributed Processes</span>

CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.

The European Joint Conferences on Theory and Practice of Software (ETAPS) is a confederation of (currently) four computer science conferences taking place annually at one conference site, usually end of March or early April. Three of the four conferences are top ranked in software engineering and one (ESOP) is top ranked in programming languages.

TAPAs is a tool for specifying and analyzing concurrent systems. Its aim is to support teaching of process algebras. Systems are described as process algebra terms that are then mapped to labeled transition systems (LTSs). Properties can be verified by checking equivalences between concrete and abstract system descriptions or by model checking temporal formulas over the obtained LTS. A key feature of TAPAs that makes it particularly suited for teaching is that it maintains a consistent graphical and textual representation of each system. After a change in the graphic notation, the textual representation is updated immediately; but after textual modifications, the update of the graphical representation has to be manually triggered.

<span class="mw-page-title-main">Marta Kwiatkowska</span> British computer scientist

Marta Zofia Kwiatkowska is a Polish theoretical computer scientist based in the United Kingdom.

CPAchecker is a framework and tool for formal software verification, and program analysis, of C programs. Some of its ideas and concepts, for example lazy abstraction, were inherited from the software model checker BLAST. CPAchecker is based on the idea of configurable program analysis which is a concept that allows expression of both model checking and program analysis with one formalism. When executed, CPAchecker performs a reachability analysis, i.e., it checks whether a certain state, which violates a given specification, can potentially be reached.

Bernhard Rumpe is a German computer scientist, professor of computer science and head of the Software Engineering Department at the RWTH Aachen University. His research focusses on "technologies, methods, tools ... necessary to create software in the necessary quality that is as efficient and sustainable as possible."

<span class="mw-page-title-main">Joost-Pieter Katoen</span> Dutch theoretical computer scientist

Joost-Pieter Katoen is a Dutch theoretical computer scientist based in Germany. He is distinguished professor in Computer Science and head of the Software Modeling and Verification Group at RWTH Aachen University. Furthermore, he is part-time associated to the Formal Methods & Tools group at the University of Twente.

<span class="mw-page-title-main">Doron A. Peled</span> Israeli computer scientist

Doron A. Peled is a computer science Professor at Bar-Ilan University. His research interests include formal methods, model checking, program synthesis and runtime verification. With Edmund M. Clarke and Orna Grumberg, he is the coauthor of the book Model Checking and the author of the book Software Reliability Methods.

Scott A. Smolka is a SUNY Distinguished Professor in the Department of Computer Science at Stony Brook University, Stony Brook, New York.

<span class="mw-page-title-main">Ofer Strichman</span>

Ofer Strichman is a professor of computational logic and computer science at the Davidson Industrial Engineering and Management, Technion – Israel Institute of Technology. He holds the Joseph Gruenblat chair in production engineering.

References

  1. 1 2 Steffen, Bernhard. "CV" (PDF). Retrieved 21 February 2022.
  2. ↑ Cleaveland, Rance; Parrow, Joachim; Steffen, Bernhard (1993). "The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems". ACM Transactions on Programming Languages and Systems. 15: 36–72. CiteSeerX   10.1.1.35.8585 . doi:10.1145/151646.151648. S2CID   14200624.
  3. ↑ van Glabbeek, Rob J.; Smolka, Scott A.; Steffen, Bernhard (1995). "Reactive, generative, and stratified models of probabilistic processes". Information and Computation. 121: 59–80. doi: 10.1006/inco.1995.1123 . S2CID   180902.
  4. 1 2 Springer. "STTT Journal Page".
  5. 1 2 "TACAS Website".
  6. 1 2 "ETAPS Website".
  7. 1 2 "ISoLA Conference Website".
  8. ↑ "RERS Website".
  9. ↑ SpringerLink. "Lecture Notes in Computer Science".
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.