Deutsche Version

M. Oliver Möller: Online Available Publications
(in time-reversed order - further up means newer)

• (single-authored) 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)
• (with Harald Rueß and 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)
• (with Alexandre David and 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)
• (with Gerd Behrman, Alexandre David, Kim G. Larsen, Paul Pettersson, and 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 )
• (with Alexandre David and 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)
• (with 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 )
• (with Harald Rueß) Solving Bit-Vector Equations
  in Formal Methods in Computer-Aided Design FMCAD'98, allows variable bit-vector size.
  (abstract, .ps.gz, bibTeX)
• (with 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: Structure and Hierarchy in Real-Time Systems,
  submitted 20 February 2002, (successfully) defended in Århus, 19 April 2002.
  (abstract, Zusammenfassung (Deutsch), .ps.bz2, .ps.gz, (hyperlinked).pdf, bibTeX), see also the BRICS pages.
  For printing it is suggested to use the .ps versions and print A5 booklets with the script shufflea5, e.g., use
    shufflea5 -d 32 thesis-omoeller.ps.gz
• (with Harald Rueß and Maria Sorea)
  Predicate Abstraction for Dense Real-Time Systems, BRICS report series, 27pp, see also the BRICS site.
  (abstract, .ps.gz, .pdf, bibTeX).
• (with Tobias Amnell, Alexandre David, Elena Fersman, Paul Pettersson, and 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 )
• (with Alexandre David)
  From HUppaal to Uppaal - a translation from hierarchical timed automat to flat timed automata, BRICS report series BRICS-RS-01-11, 40pp, see also the BRICS site;
  there exists a reference implementation
  (abstract, .ps.gz, COLOR.pdf, bibTeX)
• (with 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, and 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)
• (with Rajeev Alur)
  Heuristics for Hierarchical Partitioning with Application to Model Checking, BRICS report series, 30pp, see also the BRICS site
  (abstract, .ps.gz, .pdf, bibTeX).
• (with 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 also the BRICS site.
  (abstract, .ps.gz, .dvi.gz, .pdf, bibTeX)
• Diploma Thesis: Solving Bit-Vector Equations - A Decision Procedure for Hardware Verification - see also the Ulm 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 held in Cambridge on 9 February 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)