System Software and Distributed Systems
AVACS  Automatic Verification and Analysis of Complex Systems
Carl von Ossietzky Universität Oldenburg
Contact
eike.moehlmann(at)informatik.unioldenburg.de  
Publications

[inproceedings] bibtexS. Gerwinn, E. Möhlmann, and A. Sieper, "Statistical Model Checking for Scenariobased veriﬁcation of ADAS," in Proc. Control Strategies for Advanced Driver Assistance Systems and Autonomous Driving Functions, 2017.
@inproceedings{workshop/dtvadas/GerwinnMS2017,
author = {Sebastian Gerwinn and Eike Möhlmann and Anja Sieper},
title = {Statistical Model Checking for Scenariobased veriﬁcation of ADAS},
booktitle = {Control Strategies for Advanced Driver Assistance Systems and Autonomous Driving Functions},
year = {2017},
note = {accepted},
} 
[inproceedings] bibtex  Go to documentE. Möhlmann, W. Hagemann, and A. Rakow, "Verifying a PI Controller using SoapBox and Stabhyli," in Proc. ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria, 2016, pp. 115125.
@inproceedings{workshop/arch/MohlmannHR16,
author = {Eike M{\"{o}}hlmann and Willem Hagemann and Astrid Rakow},
title = {Verifying a {PI} Controller using SoapBox and Stabhyli},
booktitle = {ARCH@CPSWeek 2016, 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, Vienna, Austria},
editor = {Goran Frehse and Matthias Althoff},
series = {EPiC Series in Computing},
volume = {43},
pages = {115125},
year = {2016},
publisher = {EasyChair},
url = {http://www.easychair.org/publications/paper/Verifying_a_PI_Controller_using_SoapBox_and_Stabhyli},
abstract = {We describe practical experiences on verifying a steering controller specification. The hybrid automaton implements a PI control rule and considers the vehicle's velocity as input from the environment. By combining the tools Stabhyli and SoapBox, we establish several safety and liveness properties for the steering controller, including convergence towards an equilibrium.},
note = {originally submitted and accepted for ARCH14},
issn = {23987340} } 
[techreport] bibtex  Go to documentW. Damm, E. Möhlmann, and A. Rakow, "A Design Framework for Concurrent Hybrid System Controllers with Safety and Stability Annotations," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 105, 2016.
@techreport{report/ATR/DammMR2016,
author = {Werner Damm and Eike M{\"o}hlmann and Astrid Rakow},
title = {A Design Framework for Concurrent Hybrid System Controllers with Safety and Stability Annotations},
institution= {SFB/TR 14 AVACS},
year = {2016},
type = {Reports of SFB/TR 14 AVACS},
number = {105},
month = {April},
note = {http://www.avacs.org},
abstract = {We present an assume guarantee framework for hybrid systems which implements design principles tailored for loosely coupled controllers of safety critical applications. To bridge the gap between design and implementation level, the framework takes into account signal latencies and potential loss of coordination messages between controllers on a common plant. Safety as well as stability properties of a controller can be derived compositionally from its subcomponents. Industrial applications usually require safety and stability properties.},
access = {open},
bibtex = {atr105.bib},
pdf = {avacs_technical_report_105.pdf},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_105.pdf},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
series = {ATR},
subproject = {H3,H4} } 
[inproceedings] bibtex  Go to documentW. Hagemann and E. Möhlmann, "Inscribing HPolyhedra in Quadrics using a Projective Generalization of Closed Sets," in Proc. Proceedings of the 27th Canadian Conference on Computational Geometry, CCCG 2015, 2015.
@inproceedings{conf/cccg/HagemannM2015a,
author = {Willem Hagemann and Eike M{\"o}hlmann},
title = {Inscribing HPolyhedra in Quadrics using a Projective Generalization of Closed Sets},
booktitle = {Proceedings of the 27th Canadian Conference on Computational Geometry, {CCCG} 2015},
location = {Kingston, Ontario, Canada},
month = {August},
year = {2015},
url = {http://research.cs.queensu.ca/cccg2015/CCCG15papers/07.pdf},
bookurl = {http://research.cs.queensu.ca/cccg2015/CCCG.pdf},
publisher = {Queen's University, Ontario, Canada},
subproject = {H3,H4},
abstract = {We present a projective generalization of closed sets, called complete projective embeddings, which allows us to inscribe Hpolyhedra in quadrics efficiently. Essentially, the complete projective embedding of a closed convex set $P \subseteq K^d$ is a double cone in $K^{d+1}$. We show that complete projective embeddings of polyhedral sets are of particular interest and already occurred in the theory of linear fractional programming. Our approach works as follows: By projective principal axis transformation the quadric is converted to a hyperboloid and then approximated by an inner (right) spherical cylinder. Now, given an inscribed Hpolytope of the spherical cross section, cylindrification of the polyhedron yields an inscribed Hpolyhedron of the spherical cylinder and, hence, of the hyperboloid. After application of the inverse base transformation this approach finally yields an inscribed set of the quadric. The crucial task of this procedure is to find an appropriate generalization of closed sets, which is closed under the involved projective transformations and allows us to recover the nonprojective equivalents to the inscribed sets obtained by our approach. It turns out that complete projective embeddings are the requested generalizations.},
} 
[inproceedings] bibtex  Go to documentE. Möhlmann, W. Hagemann, and O. E. Theel, "Hybrid Tools for Hybrid Systems  Proving Stability and Safety at Once," in Proc. Formal Modeling and Analysis of Timed Systems  13th International Conference, FORMATS 2015, Madrid, Spain, September 24, 2015, Proceedings, 2015, pp. 222239.
@inproceedings{conf/formats/MohlmannHT15,
author = {Eike M{\"{o}}hlmann and Willem Hagemann and Oliver E. Theel},
title = {Hybrid Tools for Hybrid Systems  Proving Stability and Safety at Once},
booktitle = {Formal Modeling and Analysis of Timed Systems  13th International Conference, {FORMATS} 2015, Madrid, Spain, September 24, 2015, Proceedings},
pages = {222239},
year = {2015},
month = {September},
url = {http://dx.doi.org/10.1007/9783319229751_15},
doi = {10.1007/9783319229751_15},
series = {Lecture Notes in Computer Science},
volume = {9268},
publisher = {Springer},
isbn = {9783319229744},
subproject = {H3,H4},
abstract = {Industrial applications usually require safety and stability properties. The safety property guarantees that "something bad" never happens, and the stability property guarantees that "something good" eventually happens. The analyses of both properties are usually performed in isolation. In this work, we consider analyzing both properties by a single automatic approach for hybrid systems. We basically merge analyses of both properties to exploit the knowledge gained from the analysis of each of them in the analysis of the other. We show how both analyses can be divided into multiple steps and interlocked such that both benefit from each other. In fact, we compute singlemode Lyapunov functions, unroll the hybrid system’s automaton via repeated reachability queries, and, finally, compute a global Lyapunov function. Each reachability query is simplified by exploiting the knowledge gained from the singlemode Lyapunov functions. The final computation of the global Lyapunov function is simplified by a precise characterization of the reachable states and reuses the singlemode Lyapunov functions. We provide automated tools necessary to link the analyses and report on promising experiments we performed using our new prototype tool.},
} 
[inproceedings] bibtex  Go to documentE. Möhlmann and O. E. Theel, "Breaking Dense Structures: Proving Stability of Densely Structured Hybrid Systems," in Proc. Proceedings of the 4th International Workshop on Engineering Safety and Security Systems, ESSS 2015, Oslo, Norway, June 22, 2015., 2015, pp. 4963.
@inproceedings{conf/corr/MohlmannT15,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {Breaking Dense Structures: Proving Stability of Densely Structured Hybrid Systems},
booktitle = {Proceedings of the 4th International Workshop on Engineering Safety and Security Systems, {ESSS} 2015, Oslo, Norway, June 22, 2015.},
editor = {Pang, Jun and Liu, Yang and Mauw, Sjouke},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {184},
year = {2015},
publisher = {Open Publishing Association},
pages = {4963},
doi = {10.4204/EPTCS.184.4},
ISSN = {20752180},
month = {June},
url = {http://dx.doi.org/10.4204/EPTCS.184.4},
subproject= {H4},
abstract = {Abstraction and refinement is widely used in software development. Such techniques are valuable since they allow to handle even more complex systems. One key point is the ability to decompose a large system into subsystems, analyze those subsystems and deduce properties of the larger system. As cyberphysical systems tend to become more and more complex, such techniques become more appealing. In 2009, Oehlerking and Theel presented a (de)composition technique for hybrid systems. This technique is graphbased and constructs a Lyapunov function for hybrid systems having a complex discrete state space. The technique consists of (1) decomposing the underlying graph of the hybrid system into subgraphs, (2) computing multiple local Lyapunov functions for the subgraphs, and finally (3) composing the local Lyapunov functions into a piecewise Lyapunov function. A Lyapunov function can serve multiple purposes, e.g., it certifies stability or termination of a system or allows to construct invariant sets, which in turn may be used to certify safety and security. In this paper, we propose an improvement to the decomposing technique, which relaxes the graph structure before applying the decomposition technique. Our relaxation significantly reduces the connectivity of the graph by exploiting superdense switching. The relaxation makes the decomposition technique more efficient on one hand and on the other allows to decompose a wider range of graph structures.},
} 
[techreport] bibtex  Go to documentW. Hagemann, E. Möhlmann, and O. E. Theel, "Hybrid Tools for Hybrid System: Proving Safety and Stability at once (Extended Version)," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 108, 2015.
@techreport{report/ATR/HagemannMT2015b,
author = {Willem Hagemann and Eike M{\"o}hlmann and Oliver E. Theel},
title = {Hybrid Tools for Hybrid System: Proving Safety and Stability at once (Extended Version)},
month = {September},
year = {2015},
institution= {SFB/TR 14 AVACS},
type = {Reports of SFB/TR 14 AVACS},
note = {http://www.avacs.org},
number = {108},
access = {open},
bibtex = {atr108.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
series = {ATR},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_108.pdf},
pdf = {avacs_technical_report_108.pdf},
subproject = {H3,H4},
abstract = {Industrial applications usually require safety and stability properties. The safety property guarantees that "something bad" never happens, and the stability property guarantees that "something good" eventually happens. The analyses of both properties are usually performed in isolation. In this work, we consider analyzing both properties by a single automatic approach for hybrid systems. We basically merge analyses of both properties to exploit the knowledge gained from the analysis of each of them in the analysis of the other. We show how both analyses can be divided into multiple steps and interlocked such that both benefit from each other. In fact, we compute singlemode Lyapunov functions, unroll the hybrid system's automaton via repeated reachability queries, and, finally, compute a global Lyapunov function. Each reachability query is simplified by exploiting the knowledge gained from the singlemode Lyapunov functions. The final computation of the global Lyapunov function is simplified by a precise characterization of the reachable states and reuses the singlemode Lyapunov functions. We provide automated tools necessary to link the analyses and report on promising experiments we performed using our new prototype tool.},
} 
[inproceedings] bibtex  Go to documentO. Jubran, E. Möhlmann, and O. E. Theel, "Verifying Recurrence Properties in SelfStabilization by Checking the Absence of Finite Counterexamples," in Proc. Stabilization, Safety, and Security of Distributed Systems  17th International Symposium, SSS 2015, 2015, pp. 124138.
@inproceedings{conf/sss/JubranMT15,
author = {Oday Jubran and Eike M{\"{o}}hlmann and Oliver E. Theel},
title = {Verifying Recurrence Properties in SelfStabilization by Checking the Absence of Finite Counterexamples},
booktitle = {Stabilization, Safety, and Security of Distributed Systems  17th International Symposium, {SSS} 2015},
editor = {Andrzej Pelc and Alexander A. Schwarzmann},
location = {Edmonton, AB, Canada},
month = {August},
year = {2015},
pages = {124138},
url = {http://dx.doi.org/10.1007/9783319217413_9},
doi = {10.1007/9783319217413_9},
biburl = {http://dblp.unitrier.de/rec/bib/conf/sss/JubranMT15},
bibsource = {dblp computer science bibliography, http://dblp.org},
series = {Lecture Notes in Computer Science (LNCS)},
volume = {9212},
publisher = {SpringerVerlag},
bookurl = {http://dx.doi.org/10.1007/9783319217413},
isbn = {9783319217406},
subproject= {H4,S3},
abstract = {A performancerelated property of a system can be defined as the ratio of states satisfying some condition in each execution of the system, which we signify as the recurrence of the condition in the execution. In this work, we concern selfstabilization with respect to this property: the convergence to an execution that guarantees a minimum recurrence of a condition. For a system exhibiting infinite executions, it may not be straightforward to verify that the system satisfies the property, while considering the convergence as well. Towards simplifying such a verification, we show that for each system violating the property, there exists a finite execution prefix that is a counterexample with a reasonably short length. Furthermore, we exploit model checking to verify the absence of such counterexamples, to conclude that a system satisfies its property. We apply this approach by using the nuXmv model checker to analyze the service time of a selfstabilizing mutual exclusion algorithm having a finite state space, and running over many topologies.},
} 
[inproceedings] bibtex  Go to documentE. Möhlmann and O. E. Theel, "Towards CounterexampleGuided Computation of Validated Stability Certificates for Hybrid Systems," in Proc. Proceedings of the 2nd Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2014, 2014.
@inproceedings{conf/CoNaIISI/MohlmannT14,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {{Towards CounterexampleGuided Computation of Validated Stability Certificates for Hybrid Systems}},
year = {2014},
month = {November},
issn = {23469927},
editor = {Marcelo M. Marciszack and Roberto M. Mu{\~{n}}oz and Mario A. Groppo},
booktitle = {Proceedings of the 2nd Congreso Nacional de Ingeniería Inform{\'{a}}tica / Aplicaciones Inform{\'{a}}ticas y de Sistemas de Informaci{\'{o}}n, CoNaIISI 2014},
location = {San Luis, Argentina},
publisher = {Red de Carreras de Ingenier{\'{i}}a Inform{\'{a}}tica / Sistemas de Informati{\'{o}}n (RIISIC)},
volume = {2},
issn = {23469927},
url = {http://www.informatik.unioldenburg.de/~eikemoe/pubs/CoNaIISI_123.pdf},
abstract = {We propose a method to obtain trustable Lyapunovbased certificates of stability for hybrid systems. A hybrid system is a system exhibiting discretetime as well as continuoustime behaviors, e.g. embedded systems within a physical environment. Stability is a property which ensures that a system starting in any possible state will reach a desired state and remain there. Such systems are particularly useful when a certain autonomous operation is required, e.g. keeping a certain temperature or speed of a chemical reaction or steering a vehicle over a predefined track. Stable hybrid systems are extremely valuable because if an error disturbs their normal operation, they automatically "steer back" to normal operation. Stability can be certified by finding a socalled Lyapunov function. The search for this kind of functions usually involves solving systems of constraints. The stateoftheart in Lyapunovbased stability verification is to use numerical methods to solve systems of inequalities, which if solvable indicate stability. We propose to use SatisfiabilityModuloTheory (SMT) methods to (a) validate the results of a numerical solver and (b) use counterexamples to guide the numerical solver towards a valid solution.},
} 
[techreport] bibtex  Go to documentW. Damm, W. Hagemann, E. Möhlmann, and A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 95, 2014.
@techreport{report/ATR/DammHMR14,
author = {Werner Damm and Willem Hagemann and Eike M{\"o}hlmann and Astrid Rakow},
title = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
institution= {SFB/TR 14 AVACS},
month = {February},
year = {2014},
type = {Reports of SFB/TR 14 AVACS},
note = {http://www.avacs.org},
number = {95},
access = {open},
bibtex = {atr095.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
series = {ATR},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_095.pdf},
pdf = {avacs_technical_report_095.pdf},
subproject = {H3,H4},
abstract = {In the search of design principles that allow compositional reasoning about safety and stability properties of hybrid controllers we examine a case study on a simplified driver assistance system for lane keeping and velocity control. We thereby target loosely coupled systems: the composed system has to accomplish a task that may depend on several of its subcomponents while little coordination between them is necessary. Our assistance system has to accomplish a comfortable centrifugal force, lane keeping and velocity control. This leads to an architecture composed of a velocity controller and a steering controller, where each controller has its local objectives and together they maintain a global objective. The steering controller makes time bounded promises about its steering, which the velocity controller uses for optimization. For this system, we deductively prove from the components' properties that the objectives of the composed system are accomplished.},
} 
[inproceedings] bibtex  Go to documentW. Damm, E. Möhlmann, and A. Rakow, "Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling," in Proc. Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, 2014, pp. 145150.
@inproceedings{conf/hybrid/DammMR14,
author = {Werner Damm and Eike M{\"o}hlmann and Astrid Rakow},
title = {Component Based Design of Hybrid Systems: A Case Study on Concurrency and Coupling},
editor = {Martin Fr{\"a}nzle and John Lygeros},
booktitle = {Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14},
location = {Berlin, Berlin, Germany},
month = {April},
year = {2014},
pages = {145150},
numpages = {6},
ee = {http://doi.acm.org/10.1145/2562059.2562120},
crossref = {DBLP:conf/hybrid/2014},
publisher = {ACM},
isbn = {9781450327329},
acmid = {2562120},
url = {http://doi.acm.org/10.1145/2562059.2562120},
doi = {10.1145/2562059.2562120},
keywords = {Hybrid Systems, Automatic Verification, Stability, Safety, Composition, Interfaces, Specifications, AssumeGuarantee, ComputerAided Design},
abstract = {In the search of design principles that allow compositional reasoning about safety and stability properties of hybrid controllers we examine a case study on a simplified driver assistance system for lane keeping and velocity control. We thereby target loosely coupled systems: the composed system has to accomplish a task that may depend on several of its subcomponents while little coordination between them is necessary. Our assistance system has to accomplish a comfortable centrifugal force, lane keeping and velocity control. This leads to an architecture composed of a velocity controller and a steering controller, where each controller has its local objectives and together they maintain a global objective. The steering controller makes time bounded promises about its steering, which the velocity controller uses for optimization. For this system, we deductively prove from the components' properties that the objectives of the composed system are accomplished.},
} 
[inproceedings] bibtex  Go to documentE. Möhlmann and O. E. Theel, "Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems," in Proc. Proceedings of the 1th Congreso Nacional de Ingeniería Informática / Aplicaciones Informáticas y de Sistemas de Información, CoNaIISI 2013, 2013.
@inproceedings{conf/CoNaIISI/MohlmannT13,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {{Towards Automatic Detection of Implicit Equality Constraints in Stability Verification of Hybrid Systems}},
booktitle = {Proceedings of the 1th Congreso Nacional de Ingeniería Inform{\'{a}}tica / Aplicaciones Inform{\'{a}}ticas y de Sistemas de Informaci{\'{o}}n, CoNaIISI 2013},
year = {2013},
url = {http://conaiisi.frc.utn.edu.ar/PDFsParaPublicar/1/schedConfs/1/1045041DR.pdf},
location = {C{\'{o}}rdoba, C{\'{o}}rdoba, Argentina},
keywords = {Hybrid Systems; Automatic Verification; Stability; Lyapunov Theory; Optimization; SumsofSquares},
editor = {Marcelo M. Marciszack and Roberto M. Mu{\~{n}}oz and Mario A. Groppo},
publisher = {Red de Carreras de Ingenier{\'{i}}a Inform{\'{a}}tica / Sistemas de Informati{\'{o}}n (RIISIC)},
issn = {23469927},
abstract = {We present a powerful heuristic that detects implicit equality constraints that may occur in the specification of systems of constraints in order to find Lyapunovbased certificates of stability for hybrid systems. A hybrid system is a fusion of systems exhibiting discretetime as well as continuoustime behavior, e.g.\ embedded systems within a physical environment. Stability is a property which ensures that a system starting in any possible state will reach a desired state and remain there. Such systems are particularly useful where a certain autonomous operation is required, e.g.\ keeping a certain temperature or speed of a chemical reaction or steering a vehicle over a predefined track. Stable hybrid systems are extremely valuable because after an error has disturbed their normal operation, they automatically \enquote{steer back} to normal operation. Stability can be certified by finding a socalled Lyapunov function. The search for this kind of function usually involves solving systems of inequality constraints. We have identified and implemented a heuristic that detects implicitly specified equality constraints and tries to resolve them by substitution.},
} 
[inproceedings] bibtex  Go to documentE. Möhlmann and O. E. Theel, "Stabhyli: A Tool for Automatic Stability Verification of NonLinear Hybrid Systems," in Proc. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13, 2013, pp. 107112.
@inproceedings{conf/hybrid/MohlmannT13,
author = {Eike M{\"o}hlmann and Oliver E. Theel},
title = {Stabhyli: {A} {T}ool for {A}utomatic {S}tability {V}erification of {N}on{L}inear {H}ybrid {S}ystems},
booktitle = {Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'13},
year = {2013},
pages = {107112},
url = {http://doi.acm.org/10.1145/2461328.2461347},
crossref = {DBLP:conf/hybrid/2013},
location = {Philadelphia, Pennsylvania, USA},
acmid = {2461347},
keywords = {LMIS, automatic verification, computeraided design, hybrid systems, lyapunov theory, stability, sumsofsquares},
abstract = {We present Stabhyli, a tool that automatically proves stability of nonlinear hybrid systems. Hybrid systems are systems that exhibit discrete as well as continuous behavior. The stability property basically ensures that a system exposed to a faulty environment (e.g. suffering from disturbances) will be able to regain a "good" operation mode as long as errors occur not too frequently. Stabilizing Hybrid systems are omnipresent, for instance in control applications where a discrete controller is controlling a timecontinuous process such as a car's movement or a particular chemical reaction. We have implemented a tool to automatically derive a certificate of stability for nonlinear hybrid systems. Certificates are obtained by Lyapunov theory combined with decomposition and composition techniques.},
editor = {Calin Belta and Franjo Ivancic},
publisher = {ACM},
isbn = {9781450315678},
} 
[inproceedings] bibtex  Go to documentA. Bouajjani, R. Meyer, and E. Möhlmann, "Deciding Robustness against Total Store Ordering," in Proc. Automata, Languages and Programming  38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 48, 2011, Proceedings, Part II, 2011, pp. 428440.
@inproceedings{conf/icalp/BouajjaniMM2011,
author = {Ahmed Bouajjani and Roland Meyer and Eike M{\"{o}}hlmann},
title = {Deciding Robustness against Total Store Ordering},
booktitle = {Automata, Languages and Programming  38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 48, 2011, Proceedings, Part II},
year = {2011},
pages = {428440},
url = {http://dx.doi.org/10.1007/9783642220128_34},
doi = {10.1007/9783642220128_34},
bibsource = {DBLP, http://dblp.unitrier.de},
isbn = {9783642220111},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Ji{\v{r}\'{i}}},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
volume = {6756},
abstract = {We address the problem of deciding robustness of a program against the total store ordering (TSO) relaxed memory model, i.e., of checking whether the behaviour under TSO coincides with the expected sequential consistency (SC) semantics. We prove that this problem is PSpacecomplete. The key insight is that violations to robustness can be detected on pairs of SC computations.} }
Theses

[thesis] bibtexE. Möhlmann, "Hiding Relaxed Semantics from a User  Design and Implementation of Fence Insertion Algorithms for Concurrent Programs," Master's Thesis (Diplomarbeit) , 2010.
@thesis{Moehlmann2010,
author = {Eike M{\"o}hlmann},
title = {Hiding Relaxed Semantics from a User  Design and Implementation of Fence Insertion Algorithms for Concurrent Programs},
type = {Master's Thesis ({Diplomarbeit})},
year = {2010},
school = {LIAFA and University of Oldenburg},
supervisor = {Ahmed Bouajjani and Ernst Rüdiger Olderog and Roland Meyer},
} 
[thesis] bibtex  Go to documentE. Möhlmann and J. Timmermann, "iPosix  Ein objektorientierter Kernel in C++," Bachelor's Thesis (Studienarbeit, Individuelles Project) , 2009.
@thesis{Moehlmann2009,
author = {Eike M{\"o}hlmann and Janko Timmermann},
title = {{iPosix  Ein objektorientierter Kernel in C++}},
type = {Bachelor's Thesis ({Studienarbeit, Individuelles Project})},
year = {2009},
month = SEP, school = {University of Oldenburg},
url = {http://www.svs.informatik.unioldenburg.de/download/thesis/IP20090914moehlmann_timmermanniPosix.pdf},
supervisor = {Oliver Theel and Christian Strom},
}
Reviewer Activities
 ARES 2011
 ARES 2012
 ISPA 2012
 Computers & Security 2012 (Journal)
 HSCC 2013
 ISPA 2013
 HSCC 2014
 HSCC 2015
 CDC 2015
 FORMATS 2015
 PRDC 2015
 HSCC 2016
Supervising Activities (Theses)

[thesis] bibtex  Go to documentP. Hofstee, "Konzeption und Implementierung eines VFS Buffer Caches für iPosix," Bachelor's Thesis , University of Oldenburg, 2012.
@thesis{Hofstee2012,
author = {Pascal Hofstee},
title = {Konzeption und Implementierung eines VFS Buffer Caches für iPosix},
type = {Bachelor's Thesis},
year = 2012, institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2012/konzeptionundimplementierungeinesvfsbuffercachesfueriposix/},
key = EM, } 
[thesis] bibtex  Go to documentR. Schadek, "DMCD  A Distributed Multithreaded Caching D Compiler," Master's Thesis , University of Oldenburg, 2012.
@thesis{Schadek2012,
author = {Robert Schadek},
title = {DMCD  A Distributed Multithreaded Caching D Compiler},
type = {Master's Thesis},
year = 2012, institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {https://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2012/dmcdadistributedmultithreadingcachingdcompiler/},
pdf = {http://www.svs.informatik.unioldenburg.de/download/thesis/robert_schadek_dmcd.pdf},
key = EM, } 
[thesis] bibtex  Go to documentC. Huelsen, "Optimale Replikation," Master's Thesis , University of Oldenburg, 2013.
@thesis{Huelsen2013,
author = {Christian Huelsen},
title = {Optimale Replikation},
type = {Master's Thesis},
year = {2013},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2013/optimalereplikation/},
key = EM, } 
[thesis] bibtex  Go to documentE. Bockhorst, "Entwicklung einer automatischen Wasserqualitaetsprüfstation," Bachelor's Thesis , University of Oldenburg, 2013.
@thesis{Bockhorst2013,
author = {Eike Bockhorst},
title = {Entwicklung einer automatischen Wasserqualitaetsprüfstation},
type = {Bachelor's Thesis},
year = {2013},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2013/entwicklungeinerautomatischenwasserqualitaetspruefstation/},
key = EM, } 
[thesis] bibtex  Go to documentJ. S. Becker, "Regionentreue Algorithmen," Bachelor's Thesis , University of Oldenburg, 2013.
@thesis{Becker2013,
author = {Jan Steffen Becker},
title = {Regionentreue Algorithmen},
type = {Bachelor's Thesis},
year = {2013},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2013/regionentreuealgorithmen/},
key = EM, } 
[thesis] bibtex  Go to documentM. Hacker, "Entwicklung eines selbststabilisierenden Sensornetzwerkes," Bachelor's Thesis , University of Oldenburg, 2013.
@thesis{Hacker2013,
author = {Marius Hacker},
title = {Entwicklung eines selbststabilisierenden Sensornetzwerkes},
type = {Bachelor's Thesis},
year = {2013},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2013/entwicklungeinesselbststabilisierendensensornetzwerkes/},
key = EM, } 
[thesis] bibtex  Go to documentA. Wrasmann, "Tester für Synchronisationsprobleme," Bachelor's Thesis , University of Oldenburg, 2014.
@thesis{Wrasmann2014,
author = {Andreas Wrasmann},
title = {Tester für Synchronisationsprobleme},
type = {Bachelor's Thesis},
year = {2014},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2014/testerfuersynchronisationsprobleme/},
key = EM, } 
[thesis] bibtex  Go to documentB. Hullmann, "Entwurf und Implementierung einer kamerabasierten, augengesteuerten Eingabemöglichkeit für graphische Benutzeroberflächen," Bachelor's Thesis , University of Oldenburg, 2014.
@thesis{Hullmann2014,
author = {Bjoern Hullmann},
title = {Entwurf und Implementierung einer kamerabasierten, augengesteuerten Eingabemöglichkeit für graphische Benutzeroberflächen},
type = {Bachelor's Thesis},
year = {2014},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {https://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2014/augengesteuertebedienung/},
key = EM, } 
[thesis] bibtex  Go to documentM. Luebke, "Konstruktion und Aufbau eines fehlertoleranten, autonomen Rasenmähroboters," Master's Thesis (Diplomarbeit) , University of Oldenburg, 2014.
@thesis{Luebke2014,
author = {Michael Luebke},
title = {Konstruktion und Aufbau eines fehlertoleranten, autonomen Rasenm{\"a}hroboters},
type = {Master's Thesis ({Diplomarbeit})},
year = {2014},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2014/konstruktionundaufbaueinesautonomenfehlertolerantenrasenmaehroboters/},
key = EM, } 
[thesis] bibtex  Go to documentS. Reichel, "Running a standard Linux distribution on a smartphone," Master's Thesis , University of Oldenburg, 2015.
@thesis{Reichel2014,
author = {Sebastian Reichel},
title = {Running a standard Linux distribution on a smartphone},
type = {Master's Thesis},
year = {2015},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {https://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2015/runningastandardlinuxdistributiononasmartphone/},
key = EM, } 
[thesis] bibtex  Go to documentS. Jakubowski, "Entwurf und Implementierung eines prototypischen WebShops zur Erfassung und Abwicklung von Steckperlenbilderbestellungen," Master's Thesis , University of Oldenburg, 2015.
@thesis{Jakubowski2015,
author = {Simon Jakubowski},
title = {Entwurf und Implementierung eines prototypischen WebShops zur Erfassung und Abwicklung von Steckperlenbilderbestellungen},
type = {Master's Thesis},
year = {2015},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {http://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2015/webshopfuersteckperlenbilder/},
key = EM, } 
[thesis] bibtex  Go to documentP. Zschoche, "Automatisierte Erkennung und Eliminierung impliziter Äquivalenzen in quantifizierten nichtlinearen Ungleichungssystemen zur Stabilitätsverifikation hybrider Systeme mittels LyapunovTheorie," Bachelor's Thesis , University of Oldenburg, 2015.
@thesis{Zschoche2015,
author = {Philipp Zschoche},
title = {Automatisierte Erkennung und Eliminierung impliziter {\"A}quivalenzen in quantifizierten nichtlinearen Ungleichungssystemen zur Stabilit{\"a}tsverifikation hybrider Systeme mittels LyapunovTheorie},
year = {2015},
type = {Bachelor's Thesis},
institution = {University of Oldenburg},
supervisor = {Oliver Theel and Eike M{\"o}hlmann},
url = {https://www.unioldenburg.de/informatik/svs/lehre/abschlussarbeiten/2015/automatisierteerkennungundeliminierungimpliziteraquivalenzeninquantifiziertennichtlinearenungleichungssystemenzurstabilitatsverifikationhybridersystememittelslyapunovtheorie/},
key = EM, }