Publications 2002

Rafael Accorsi and David Basin and Luca Viganò.
Modal Specifications of Trace-Based Security Properties.
In Proceedings of the Second International Workshop on Security of Mobile Multiagent Systems (SEMAS-2002).
Research Report University Saarbrücken, 2002.
[Downloadabstract (TXT, 982 Bytes) | DownloadBibTeX (TXT, 1 KB) | DownloadPDF (PDF, 230 KB) | Downloadgzip'ed Postscript (GZ, 97 KB)]

Alessandro Armando and David Basin and Mehdi Bouallagui and Yannick Chevalier and Luca Compagna and Sebastian Mödersheim and Michael Rusinowitch and Mathieu Turuani and Luca Viganò and Laurent Vigneron.
The AVISS Security Protocol Analysis Tool.
In Computer-Aided Verification CAV'02. Lecture Notes in Computer Science 2404 Springer-Verlag, 2002.
[Downloadabstract (TXT, 770 Bytes) | DownloadBibTeX (TXT, 1 KB) | DownloadPDF (PDF, 270 KB) | Downloadgzip'ed Postscript (GZ, 58 KB)]

Abdelwaheb Ayari and David Basin.
Qubos: Deciding Quantified Boolean Logic using Propositional Satisfiability Solvers.
In Formal Methods in Computer-Aided Design, Fourth International Conference, FMCAD 2002.Springer-Verlag, 2002.
[Downloadabstract (TXT, 547 Bytes) | DownloadBibTeX (TXT, 925 Bytes) | DownloadPDF (PDF, 208 KB) | Downloadgzip'ed Postscript (GZ, 98 KB)]

Abdelwaheb Ayari and David Basin and Felix Klaedtke.
Decision Procedures for Inductive Boolean Functions based on Alternating Automata.
In Theoretical Computer Science, 2002.
[Downloadabstract (TXT, 764 Bytes) | DownloadBibTeX (TXT, 1 KB) | DownloadPDF (PDF, 401 KB) | Downloadgzip'ed Postscript (GZ, 169 KB)]

David Basin and Stefan Friedrich and Marek Gawkowski and Joachim Posegga.
Bytecode Model Checking: An Experimental Analysis.
In Model Checking Software, 9th International SPIN Workshop.LNCS, 2318.
Springer-Verlag, 2002.
[Downloadabstract (TXT, 620 Bytes) | DownloadBibTeX (TXT, 620 Bytes) | DownloadPDF (PDF, 255 KB)| Downloadgzip'ed Postscript (GZ, 105 KB)]

David Basin and Stefan Friedrich and Marek Gawkowski.
Verified Bytecode Model Checkers.
In Theorem Proving in Higher Order Logics (TPHOLs'02).LNCS, 2410. Springer-Verlag, 2002.
[Downloadabstract (TXT, 897 Bytes) | DownloadBibTeX (TXT, 1 KB) | DownloadPDF (PDF, 261 KB) | Downloadgzip'ed Postscript (GZ, 104 KB)]

David Basin and Frank Rittinger and Luca Viganò.
A Formal Analysis of the CORBA Security Service.
In ZB 2002: Formal Specification and Development in Z and B. lncs Springer-Verlag, 2002.
[Downloadabstract (TXT, 937 Bytes) | DownloadBibTeX (TXT, 2 KB) | DownloadPDF (PDF, 280 KB) | Downloadgzip'ed Postscript (GZ, 89 KB)]

K. Bender and M. Broy and I. Péter and A. Pretschner and T. Stauner.
Model based development of hybrid systems: specification, simulation, test case generation.
In Modelling, Analysis, and Design of Hybrid Systems.LNCIS, 279. Springer, 2002.
[Downloadabstract (TXT, 786 Bytes) | DownloadBibTeX (TXT, 1 KB)]

Achim D. Brucker and Stefan Friedrich and Frank Rittinger and Burkhart Wolff.
HOL-Z 2.0: A Proof Environment for Z-Specifications.
In FMTOOLS 2002. Technical Report 2002-11, 2002.
[Downloadabstract (TXT, 482 Bytes) | DownloadBibTeX (TXT, 1 KB) | DownloadPDF (PDF, 146 KB)]

Achim D. Brucker and Frank Rittinger and Burkhart Wolff.
The CVS-Server Case Study: A Formalized Security Architecture.
In FM-TOOLS 2002. Technical Report 2002-11, 2002.
[Downloadabstract (TXT, 1007 Bytes) | DownloadBibTeX (TXT, 2 KB) | DownloadPDF (PDF, 607 KB)]

Achim D. Brucker and Frank Rittinger and Burkhart Wolff.
A CVS-Server Security Architecture - Concepts and Formal Analysis.
Albert-Ludwigs-Universität Freiburg, Technical Report 182, 2002.
[Downloadabstract (TXT, 1 KB) | DownloadBibTeX (TXT, 2 KB) | DownloadPDF (PDF, 902 KB) | Downloadgzip'ed Postscript (GZ, 836 KB)]

Achim D. Brucker and Burkhart Wolff.
A Proposal for a Formal OCL Semantics in Isabelle/HOL.
In Theorem Proving in Higher Order Logics. lncs 2410, Springer-Verlag, 2002.
[Downloadabstract (TXT, 607 Bytes) | DownloadBibTeX (TXT, 2 KB) | DownloadPDF (PDF, 596 KB) | Downloadextended (PDF, 250 Bytes)]

Achim D. Brucker and Burkhart Wolff.
HOL-OCL: Experiences, Consequences and Design Choices.
In UML 2002: Model Engineering, Concepts and Tools. lncs 2460, Springer-Verlag, 2002.
[Downloadabstract (TXT, 608 Bytes) | DownloadBibTeX (TXT, 2 KB) | DownloadPDF (PDF, 567 KB)]

Torsten Lodderstedt and David Basin and Jürgen Doser.
SecureUML: A UML-Based Modeling Language for Model-Driven Security.
In The unified modeling language: model engineering, concepts, and tools; 5th international., 2460. Springer, 2002.
[Downloadabstract (TXT, 762 Bytes) | DownloadBibTeX (TXT, 1 KB) | DownloadPDF (PDF, 90 KB)]

João Rasga and Amílcar Sernadas and Cristina Sernadas and Luca Viganò.
Labelled Deduction over Algebras of Truth-Values.
In Frontiers of Combining Systems 4 (Proceedings of FroCoS'2002). LNCS 2309 Springer-Verlag, 2002.
[Downloadabstract (TXT, 838 Bytes) | DownloadBibTeX (TXT, 1 KB) | DownloadPDF (PDF, 253 KB) | Downloadgzip'ed Postscript (GZ, 216 KB)]

João Rasga and Amílcar Sernadas and Cristina Sernadas and Luca Viganò.
Fibring Labelled Deduction Systems.
In Journal of Logic and Computation, 12 (3), pages 443-473, 2002.
[Downloadabstract (TXT, 736 Bytes) | DownloadBibTeX (TXT, 1 KB) | DownloadPDF (PDF, 297 KB) | Downloadgzip'ed Postscript (GZ, 266 KB)]

B. Schätz and A. Pretschner and F. Huber and J. Philipps.
Model-Based Development of Embedded Systems.
In Advances in Object-Oriented Information Systems.LNCS, 2426. Springer, 2002.
[Downloadabstract (TXT, 718 Bytes) | DownloadBibTeX (TXT, 1 KB)]