Publications
The layout of the preprint versions provided on this page may differ from the original versions.
- Jens Gutsfeld, Markus Müller-Olm and Christoph Ohrem.
Automata and fixpoints for asynchronous hyperproperties.
Proc. ACM Program. Lang., 5(POPL), 1–29., 2021.
doi:10.1145/3434319
Extended version with proofs on arXiv: https://arxiv.org/abs/2010.11605 - Jens Oliver Gutsfeld, Markus Müller-Olm and Christian Dielitz.
Temporal Logics with Language Parameters.
In A. Leporati, C. Martı́n-Vide, D. Shapira, & C. Zandron (Eds.), Language and Automata Theory and Applications - 15th International Conference, LATA 2021, Milan, Italy, March 1-5, 2021, Proceedings (Vol. 12638, pp. 187–199). Springer.
doi:10.1007/978-3-030-68195-1_14
Version on arXiv: https://arxiv.org/abs/1910.11594 - Jens Gutsfeld, Markus Müller-Olm and Christoph Ohrem.
Propositional Dynamic Logic for Hyperproperties.
In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 50:1–50:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
doi:10.4230/LIPIcs.CONCUR.2020.50
Extended version with proofs on arXiv: https://arxiv.org/abs/1910.10546 - Xinyu Feng, Markus Müller-Olm, Zijiang Yang.
Dependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Beijing, China, September 4-6, 2018. Proceedings. Lecture Notes in Computer Science 10998, Springer, 2018, ISBN 978-3-319-99932-6. - Jens Gutsfeld, Markus Müller-Olm and Benedikt Nordhoff.
A Branching Time Variant of CaRet.
In SPIN 2018. LNCS 10869. Springer, 2018. - Heiko Mantel, Markus Müller-Olm, Matthias Perner, Alexander Wenner.
Using Dynamic Pushdown Networks to Automate a Modular Information-flow Analysis.
In Post-Proceedings of Logic-Based Program Synthesis and Transformation (LOPSTR). July, 2015.
LNCS 9527. Springer International Publishing.
lopstr2015.pdf , Copyright Springer
Extended Version with Appendix: lopstr2015_app.pdf - Markus Müller-Olm, Helmut Seidl:
Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings. Lecture Notes in Computer Science 8723, Springer, 2014, ISBN 978-3-319-10935-0. - Benedikt Nordhoff, Markus Müller-Olm and Peter Lammich
Iterable Forward Reachability Analysis of Monitor-DPNs
In Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh and John Hatcliff: Proceedings Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday (Festschrift for Dave Schmidt), Manhattan, Kansas, USA, 19-20th September 2013, Electronic Proceedings in Theoretical Computer Science 129, pp. 384-403. http://dx.doi.org/10.4204/EPTCS.129.24, September 2013. - Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner.
Contextual Locking for Dynamic Pushdown Networks.
In Proceedings of SAS 2013 (20th Static Analysis Symposium), LNCS 7935. Springer, 2013.
sas13.pdf , Copyright Springer - Andrea Flexeder, Markus Müller-Olm, Michael Petter, and Helmut Seidl.
Fast Interprocedural Linear Two Variable Equalities.
ACM Trans. Program. Lang. Syst. (TOPLAS) 33(6), December 2011. - Martin Schwarz, Helmut Seidl, Vesal Vojdani, Markus Müller-Olm, and Peter Lammich.
Static Analysis of Interrupt-Driven Programs Synchronized via the Priority Ceiling Protocol.
In Proc. of POPL 2011 (Principles of Programming Languages), January 26-28, 2011, Austin, Texas, USA. - Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner.
Join-Lock-Sensitive Forward Reachability Analysis of Concurrent Programs with Dynamic Process Creation.
In Proc. of VMCAI 2011 (Verification, Model Checking, and Abstract Interpretation), LNCS 6538, pages 199-213. Springer, 2011. vmcai11.pdf , Copyright Springer
Extended Version with proofs: vmcai11extended.pdf - Nicholas Kidd, Peter Lammich, Tayssir Touili and Thomas Reps.
A decision procedure for detecting atomicity violations for communicating processes with locks.
In International Journal on Software Tools for Technology Transfer (STTT), Volume 13, Number 1, 37-60
sttt10_atomicity.pdf , Copyright Springer - Peter Lammich and Andreas Lochbihler.
The Isabelle Collections Framework.
In Proceedings of ITP 2010, LNCS 6172, pages 339-354. Springer, 2010.
itp10.pdf , Copyright Springer - Alexander Wenner.
Weighted Dynamic Pushdown Networks.
In Proceedings of 19th European Symposium on Programming (ESOP 2010), LNCS 6012, pages 590-609. Springer, 2010.
esop10.pdf , Copyright Springer - Peter Lammich
Isabelle Collections Framework.
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, November 2009.
Formal proof development.
http://afp.sourceforge.net/entries/Collections.shtml - Peter Lammich
Tree Automata.
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, November 2009.
Formal proof development.
http://afp.sourceforge.net/entries/Tree-Automata.shtml - Peter Lammich, Markus Müller-Olm, and Alexander Wenner.
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints.
In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification (Proc. 21st International Concerence, CAV'09), LNCS 5643, pages 525-539. Springer, 2009.
cav09.ps.gz or cav09.pdf , Copyright Springer
Most of the results in this paper have been verified with the theorem prover Isabelle/HOL. For details see the technical report. - Nicholas Kidd, Peter Lammich, Tayssir Touili, and Thomas Reps
A decision procedure for detecting atomicity violations for communicating processes with locks.
In Proceedings of SPIN Workshop, 2009
spin09.atomicity.pdf , Copyright Springer
Extended version with proofs: tr-atomicity.pdf - Neil D. Jones and Markus Müller-Olm (Eds.).
Verification, Model Checking, and Abstract Interpretation.
10th International Conference, VMCAI 2009, Savannah, GA, USA, January 2009, Proceedings.
LNCS 5403. Springer, 2009.
Available online from SpringerLink (access to full papers is restricted to LNCS subscribers) , Copyright Springer - Peter Lammich
Isabelle Formalization of Hedge-Constrained pre* and DPNs with Locks.
Technical Report, Univ. of Münster, January 2009.
Contains proofs for most of the results of our CAV'09 paper.
Proof Document Proof Outline (Proofs skipped) Sources - Peter Lammich and Markus Müller-Olm.
Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors.
In Maria Alpuente and German Vidal, editors, Static Analysis (Proc. 15th International Symposium, SAS 2008), LNCS 5079, pages 205-220. Springer, 2008.
sas08.ps.gz or sas08.pdf , Copyright Springer
Technical Report version with appendices, March 2008:
tr-conflict-analysis.ps or tr-conflict-analysis.pdf - Markus Müller-Olm and Helmut Seidl.
Upper Adjoints for Fast Inter-Procedural Variable Equalities.
In Sophia Drossopoulou, editor, Programming Languages and Systems (Proc. 17th European Symposium on Programming, ESOP 2008), LNCS 4960, pages 178-192. Springer, 2008.
esop08.ps.gz or esop08.pdf , Copyright Springer - Peter Lammich and Markus Müller-Olm.
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors.
In G. Klein, T. Nipkow, and L. Paulson, editors, The Archive of Formal Proofs, December 2007.
Formal proof development.
http://afp.sourceforge.net/entries/Program-Conflict-Analysis.shtml - Markus Müller-Olm and Helmut Seidl.
Analysis of Modular Arithmetic.
ACM Trans. Program. Lang. Syst. (TOPLAS) 29(5), August 2007.
toplas-preprint-modulo.pdf - Peter Lammich and Markus Müller-Olm.
Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures.
In L. Caires, V.T. Vasconcelos, editors, CONCUR 2007: Concurrency Theory, LNCS 4703, pages 287-302. Springer, 2007.
concur07.ps.gz or concur07.pdf , Copyright Springer
Version with appendix: concur07-extend.ps.gz or concur07-extend.pdf - Markus Müller-Olm.
Variations on Constants: Flow Analysis of Sequential and Parallel Programs.
Monograph, LNCS 3800, Springer, 2006. - Markus Müller-Olm, Michael Petter, and Helmut Seidl.
Interprocedurally Analyzing Polynomial Identities.
In B. Durand and W. Thomas, editors, STACS 2006 (Symposium on Theoretical Aspects of Computer Science), LNCS 3884, pages 50-67. Springer, 2006.
stacs06.ps.gz or stacs06.pdf , Copyright Springer - Ahmed Bouajjani, Markus Müller-Olm, and Tayssir Touili.
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems.
In Martin Abadi and Luca de Alfaro, editors, Concurrency Theory (Proc. 16th International Conference, CONCUR 2005), LNCS 3653, pages 473-487. Springer, 2005.
concur05.ps.gz or concur05.pdf , Copyright Springer
Extended version with proofs: concur05-long.ps.gz or concur05-long.pdf - Markus Müller-Olm and Helmut Seidl.
A Generic Framework for Interprocedural Analysis of Numerical Properties.
In Chris Hankin and Igor Siveroni, editors, Static Analysis (Proc. 12th International Symposium, SAS 2005), LNCS 3672, pages 235-250. Springer, 2005.
sas05.ps.gz or sas05.pdf , Copyright Springer - Markus Müller-Olm, Helmut Seidl, and Bernhard Steffen.
Interprocedural Herbrand Equalities.
In Mooly Sagiv, editor, Programming Languages and Systems (Proc. 14th European Symposium on Programming, ESOP 2005), LNCS 3444, pages 31-45. Springer, 2005.
esop05-herbrand.ps.gz or esop05-herbrand.pdf , Copyright Springer - Markus Müller-Olm and Helmut Seidl.
Analysis of Modular Arithmetic.
In Mooly Sagiv, editor, Programming Languages and Systems (Proc. 14th European Symposium on Programming, ESOP 2005), LNCS 3444, pages 46-60. Springer, 2005.
esop05-modulo.ps.gz or esop05-modulo.pdf , Copyright Springer - Markus Müller-Olm, Oliver Rüthing, and Helmut Seidl.
Checking Herbrand Equalities and Beyond.
In Radhia Cousot, editor, VMCAI 2005 (Sixth International Conference on Verification, Model Checking, and Abstract Interpretation), LNCS 3385, pages 79-96. Springer, 2005.
vmcai05.ps.gz or vmcai05.pdf , Copyright Springer - Markus Müller-Olm, Helmut Seidl, and Bernhard Steffen.
Interprocedural Analysis (Almost) for Free.
Technical Report 790, Fachbereich Informatik, Universität Dortmund, July 2004.
tr-do790.ps.gz or tr-do-790.pdf - Markus Müller-Olm and Helmut Seidl.
Interprocedural Analysis of Modular Arithmetic.
Technical Report 789, Fachbereich Informatik, Universität Dortmund, July 2004.
tr-do789.ps.gz or tr-do789.pdf - Markus Müller-Olm, Oliver Rüthing, and Helmut Seidl.
Testing Herbrand Equalities and Beyond.
Technical Report 788, Fachbereich Informatik, Universität Dortmund, July 2004.
tr-do788.ps.gz or tr-do788.pdf - Markus Müller-Olm and Helmut Seidl.
A Note on Karr's Algorithm.
International Colloquium on Automata, Languages, and Programming (ICALP'04), July 12-16, 2004, Turku, Finland.
icalp04.ps.gz or icalp04.pdf , Copyright Springer - Markus Müller-Olm and Haiseung Yoo.
MetaGame: An animation tool for model-checking games.
Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), March 29-April 2, 2004, Barcelona, Spain.
tacas04.ps.gz or tacas04.pdf , Copyright Springer - Markus Müller-Olm and Helmut Seidl.
Computing polynomial program invariants.
Information Processing Letters (IPL) 91(5), pages 233-244, 2004.
(Preliminary version appeared as technical report of FernUniversität Hagen, Fachbereich Informatik, TR-310, October 2003.)
ipl-poly-preprint.ps.gz or ipl-poly-preprint.pdf ©Elsevier - Markus Müller-Olm and Helmut Seidl.
Precise interprocedural analysis through linear algebra.
Proceedings of Principles of Programming Languages (POPL'04), January 14-16, 2004, Venice, Italy.
popl04.ps.gz or popl04.pdf ©ACM - Markus Müller-Olm.
Precise interprocedural dependence analysis of parallel programs.
Theoretical Computer Science (TCS) 31(1), pages 325-388, 2004.
tcsb-979.ps.gz or tcsb-979.pdf ©Elsevier - Helmut Seidl, Varmo Vene, and Markus Müller-Olm.
Global invariants for analysing multi-threaded applications.
Proc. of Estonian Academy of Sciences: Phys., Math., volume 52, nr. 4, pages 413-436, 2003.
globinv.ps.gz or globinv.pdf ©Estonian Academy Publishers - Rudolf Berghammer and Markus Müller-Olm.
Formal development and verification of approximation algorithms using auxiliary variables.
Workshop on Logic-Based Program Development and Transformation (LOPSTR'03), August 25-27, 2003, Uppsala, Schweden. Revised version appeared in LNCS 3018, pp. 59-74. Springer 2004.
lopstr03pre.ps.gz or lopstr03pre.pdf - Markus Müller-Olm and Helmut Seidl.
Computing interprocedurally valid relations in affine programs.
Technical Report, University of Trier, January 2003.
Revised version appeared in POPL 2004 under modified title Precise Interprocedural Analysis through Linear Algebra.
affinetrtrier.ps.gz or affinetrtrier.pdf - Markus Müller-Olm.
Variations on Constants.
Habilitation thesis, Fachbereich Informatik, Universität Dortmund. August 2002.
habil.ps.gz or habil.pdf - Markus Müller-Olm and Helmut Seidl.
Polynomial constants are decidable.
In M. V. Hermenegildo and German Puebla, editors, SAS 2002 (9th Static Analysis Symposium), LNCS 2477, pages 4-19. Springer, 2002.
sas02.ps.gz or sas02.pdf , Copyright Springer - Markus Müller-Olm and Helmut Seidl.
On optimal slicing of parallel programs.
In STOC 2001 (33th ACM Symposium on Theory of Computing), pages 647-656. © ACM Press, 2001.
stoc01.ps.gz or stoc01.pdf ©ACM - Markus Müller-Olm and Oliver Rüthing.
The complexity of constant propagation.
In D. Sands, editor, ESOP 2001 (10th European Symposium on Programming), LNCS 2028, pages 190-205. Springer, 2001.
esop01.ps.gz or esop01.pdf , Copyright Springer - Markus Müller-Olm.
The complexity of copy constant detection in parallel programs.
In Afonso Ferreira and Horst Reichel, editors, STACS 2001 (Symposium on Theoretical Aspects of Computer Science), LNCS 2010, pages 490-501. Springer, 2001.
stacs01.ps.gz or stacs01.pdf , Copyright Springer - Markus Müller-Olm and Andreas Wolf.
On the translation of procedures to finite machines: Abstraction allows a clean proof.
In Gert Smolka, editor, Programming Languages and Systems: ESOP'2000, LNCS 1782, pages 290-304. Springer, 2000.
esop00.ps.gz or esop00.pdf , Copyright Springer - Martin Fränzle and Markus Müller-Olm.
Compilation and synthesis for real-time embedded controllers.
In B. Steffen and E.-R. Olderog, editors, Correct System Design: Recent Insights and Advances, LNCS 1710, pages 256-287. Springer, 1999.
hl-band.ps.gz or hl-band.pdf , Copyright Springer - Markus Müller-Olm and Andreas Wolf.
On excusable and inexcusable failures: Towards an adequate notion of translation correctness.
In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, FM'99: Formal Methods, LNCS 1709, pages 1107-1127. Springer, 1999.
fm99.ps.gz or fm99.pdf , Copyright Springer - Martin Fränzle, Wolfgang Goerigk, Burghard von Karger, and Markus Müller-Olm.
Beyond ProCoS at Kiel: A synopsis of recent research.
ProCoS WG workshop at FM'99, available from FM'99 CD-Rom, Springer, September 1999.
fm99procos.ps.gz or fm99procos.pdf - Markus Müller-Olm, David Schmidt, and Bernhard Steffen.
Model-checking: A tutorial introduction.
In A. Cortesi and G. Filé, editors, Static Analysis: SAS'99, LNCS 1694, pages 330-354. Springer, 1999.
sas99.ps.gz or sas99.pdf , Copyright Springer - Markus Müller-Olm, Bernhard Steffen, and Rance Cleaveland.
On the evolution of reactive components: A process-algebraic approach.
In Jean-Pierre Finance, editor, FASE'99, LNCS 1577, pages 161-175. Springer, 1999.
fase99.ps.gz or fase99.pdf , Copyright Springer - Markus Müller-Olm.
A modal fixpoint logic with chop.
In Christoph Meinel and Sophie Tison, editors, STACS'99, LNCS 1563, pages 510-520. Springer, 1999.
stacs99.ps.gz or stacs99.pdf - Markus Müller-Olm.
Derivation of characteristic formulae.
Electronic Notes in Theoretical Computer Science, 18:12, August 1998.
http://www.sciencedirect.com/science/article/pii/S1571066105802579?via%3Dihub.
mfcs98.ps.gz or mfcs98.pdf - Markus Müller-Olm.
Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction.
Monograph, LNCS 1283, Springer, 1997.