(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 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)