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