English version

M. Oliver Möller: Wissenschaftliche Veröffentlichungen
(je neuer ein Artikel, desto weiter oben steht er)

• (alleiniger Author) Parking can get you there faster - Model Augmentation to Speed up Real-Time Model Checking
  at Theory and Practice of Timed Systems (TPTS'2002), part of ETAPS 2002
  (abstract .ps.gz, .pdf, bibTeX)
• (mit Harald Rueß und Maria Sorea) Predicate Abstraction for Dense Real-Time Systems
  at Theory and Practice of Timed Systems (TPTS'2002), part of ETAPS 2002
  [basically a condensed version of BRICS-RS-01-44]
  (abstract, .ps.gz, .pdf, bibTeX)
• (mit Alexandre David und Wang Yi) Formal Verification of UML Statecharts with Real-time Extensions
  at FASE'2002 8.-12. April in Grenoble, France; part of ETAPS 2002
  [basically a condensed version of BRICS-RS-01-11]
  (abstract .ps.gz, .pdf, bibTeX)
• (mit Gerd Behrman, Alexandre David, Kim G. Larsen, Paul Pettersson, und Wang Yi) UPPAAL - Present and Future
  at 40th IEEE Conference on Decision and Control, December 4-7, 2001, Orlando, Florida
  (a preliminary version appeared at the Workshop on Real-Time Tools CONCUR'01)
  ( abstract, .ps.gz, .pdf, bibTeX )
• (mit Alexandre David und Wang Yi) Formal Verification of UML Statecharts with Real-time Extensions
  at The 13th Nordic Workshop on Programming Theory (NWPT'01) DTU Lyngby, Denmark, October 10-12, 2001
  [basically a condensed version of BRICS-RS-01-11]
  (extended abstract to be printed in proceedings abstract .ps.gz, .pdf, appeared in bibTeX)
• (mit Rajeev Alur) Heuristics for Hierarchical Partitioning with Application to Model Checking
  in Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME'01
  (abstract, .ps.gz, .pdf, bibTeX )
• (mit Harald Rueß) Solving Bit-Vector Equations
  in Formal Methods in Computer-Aided Design FMCAD'98, allows variable bit-vector size.
  (abstract, .ps.gz, bibTeX)
• (mit David Cyrluk, Harald Rueß) An Efficient Decision Procedure for the Theory of Fixed-Sized Bitvectors
  in Conference of Computer-Aided Verification (CAV'97)
  (abstract, .ps.gz, bibTeX)

• PhD thesis (Doktorarbeit): Structure and Hierarchy in Real-Time Systems,
  eingereicht am 20 Februar 2002, (erfolgreich) verteidigt in Århus, 19 April 2002.
  (Zusammenfassung (Deutsch), abstract (Englisch), .ps.bz2, .ps.gz, (hyperlinked).pdf, bibTeX), siehe dazu auch die BRICS Seiten.
  Zum Ausdrucken wird die .ps Version und ein doppelseitige, gefaltete Din A5 Format empfohlen. Dazu kann das Skript shufflea5 verwendet werden, z.B. mittels
    shufflea5 -d 32 thesis-omoeller.ps.gz
• (mit Harald Rueß und Maria Sorea)
  Predicate Abstraction for Dense Real-Time Systems, BRICS report series, 27pp, siehe auch die BRICS site.
  (abstract, .ps.gz, .pdf, bibTeX).
• (mit Tobias Amnell, Alexandre David, Elena Fersman, Paul Pettersson, und Wany Yi)
  Tools for Real-Time UML: Formal Verification and Code Synthesis, workshop paper at Specification, Implementation and Validation of Object-oriented Embedded Systems (SIVOES'2001) 18-22 June 2001, Budapest Hungary
  (abstract, .ps.gz, .pdf )
• (mit Alexandre David)
  From HUppaal to Uppaal - a translation from hierarchical timed automat to flat timed automata, BRICS report series BRICS-RS-01-11, 40pp, siehe auch die BRICS site;
  es gibt eine reference implementation
  (abstract, .ps.gz, COLOR.pdf, bibTeX)
• (mit Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D'Argenio, Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G. Larsen, Paul Pettersson, Carsten Weise, und Wang Yi)
  UPPAAL - Now, Next, and Future In Proceedings of Modeling and Verification of Parallel Processes (MOVEP'2k), Nantes, France, June 19 to 23, 2000. LNCS Tutorial 2067, pages 100-125, F. Cassez, C. Jard, B. Rozoy, and M. Ryan (Eds.), 2001
  (abstract, .ps.gz, .pdf, bibTeX)
• (mit Rajeev Alur)
  Heuristics for Hierarchical Partitioning with Application to Model Checking, BRICS report series, 30pp, siehe auch BRICS site
  (abstract, .ps.gz, .pdf, bibTeX).
• (mit Harald Rueß)
  Solving Bit-Vector Equations of Fixed and Non-Fixed Size, BRICS report series, RS-99-18, 18pp
  slightly revised version of the FMCAD'98 publication, siehe auch die BRICS site.
  (abstract, .ps.gz, .dvi.gz, .pdf, bibTeX)
• Diplomarbeit, März 1998: Solving Bit-Vector Equations - A Decision Procedure for Hardware Verification - siehe auch die Ulmer site
  (abstract, .pdf, .ps, .ps.gz, bibTeX)

• "Structure and Hierarchy in Real-Time Systems"
  PhD defense Århus, 19 April 2002
  (.pdf)
• "Predicate Abstraction for Dense Real-Time Systems"
  workshop talk at TPTS, Grenoble, 7 April 2002
  (.pdf)
• "Parking Can Get You There Faster - Model Augmenation to Speed Up Real-Time Model Checking"
  workshop talk at TPTS, Grenoble, 7 April 2002
  (.pdf)
• "Predicate Abstraction for Dense Real-Time Systems"
  seminar talk at Aalborg, 7 February 2002
  (.pdf)
• "Uppaal - Present and Future"
  paper presentation at CDC'01, 6 December 2001, Orlando, Florida, USA
  (.pdf)
• "The WOODDES Project: Building Better Embedded Systems"
  overview talk at the Network in Test and Modeling of Software (ToMaS), Aalborg 28 Nov 2001
  (.pdf)
• "Formal Verification of UML Statecharts with Real-time Extensions"
  Paper presentation at NWPT'2001, 10 October 2001
  (.pdf)
• "Hierarchical Partitioning (really) helps - from flat structures to hierarchies"
  Paper presentation at CHARME'2001, 4 September 2001
  (.pdf)
• "Uppaal now, next, and future - meet a family of model-checkers"
  Talk at CONCUR'2001 Workshop Real-Time Tools on 20 August 2001
  (.pdf)
• "The Concurrency Workbench: making CCS run"
  Tool Talk gegeben in Cambridge am 9 Februar 2001
  (.pdf)
• "Automation for Formal Verification: Exploiting Structure"
  BRICS Progress Report presentation, 24 February 2000
  (.pdf)
• "Solving Bit-Vector Equations - Concepts for fixed and non-fixed length"
  from the FMCAD'98 presentation
  (.ps.gz)
• "An Efficient Decision Procedure for the Theory of Fixed-sized Bit-Vectors"
  from the CAV'97 presentation
  (.ps.gz)