![[I2 logo]](../../../Images/i2.gif)
![[RWTH logo]](../../../Images/rwth-rot90.gif)
(Informatik 2)
HomeNewsJobsContactStaffTeachingResearchMOVES SeminarDFG-GK AlgoSynCS ChairsLuFG I2
Model Checking von Software
Seminar zur Praktischen und Theoretischen Informatik
Wintersemester 2001/02
Die zunehmende Bedeutung des Model Checking als methodischer Ansatz zur Hardwareverifikation und die Probleme mit der Erstellung korrekter Computerprogramme motivieren die Anwendung entsprechender Methoden auf Softwaresysteme. Dieses wirft interessante Probleme auf, sowohl bei den eigentlichen Model Checking-Algorithmen als auch bei unterstützenden Techniken. Hier sind in erster Linie Programmanalysen und -transformationen zu nennen, welche den (gewöhnlich unendlichen) Zustandsraum des Programms durch Abstraktion von Datenzuständen und Reduktion von Kontrollzuständen in einen endlichen Bereich überführen.In diesem Seminar sollen konkrete Model Checking-Ansätze sowie entsprechende Tools für die Programmiersprachen
- C,
- Erlang und
- Java
Vorbesprechung
Diese findet amMontag, dem 16. Juli 2001, um 14:00 Uhr im Seminarraum des Lehrstuhlsstatt.
Themen
Die folgende Tabelle gibt eine Übersicht der Einzelthemen. Die Vorträge finden jeweilsmontags um 14:00 Uhr im Seminarraum des Lehrstuhls für Informatik IIstatt.
Hier finden Sie allgemeine Hinweise zur Ausarbeitung und zum Vortrag.
| Nr. | Datum | Thema | Literatur | Referent(in) | Betreuer |
|---|---|---|---|---|---|
| Verifikation zur Laufzeit | |||||
| 1 | 22.10.01 | Black Box Checking | [PVY99] | Arne Schmitz | Benedikt Bollig |
| 2 | 29.10.01 | LTL-Checking mit alternierenden Automaten | [FS01] | Ralph Sluiters | Martin Leucker |
| Abstraktionstechniken | |||||
| 3 | 05.11.01 | Boolesche Abstraktion | |||
| 4 | 12.11.01 | Program Slicing | [Tip95] | Luan Ahmeti | Thomas Noll |
| 5 | 19.11.01 | Tabellengesteuerte Abstraktion | [HS99] | Sebastian Lohmann | Thomas Noll |
| - | 26.11.01 | ||||
| 6 | 03.12.01 | Korrektheit von Abstraktionen | [LGS95] | Wong Karianto | Martin Leucker |
| Verifikation von C-Programmen | |||||
| 7 | 10.12.01 | SLAM | [BMM01, BPR00, BR01] | Stefan Raffelsieper | Benedikt Bollig |
| 8 | 17.12.01 | VeriSoft | [God97] | Lars Helge Haß | Benedikt Bollig |
| 9 | 07.01.02 | Verifikation verteilter C-Programme | [Hol01] | Tim Schwerdtner | Benedikt Bollig |
| Verifikation von Erlang-Programmen | |||||
| 10 | 07.01.02 | Model Checking mit abstrakter Interpretation | |||
| Verifikation von Java-Programmen | |||||
| 11 | 14.01.02 | Bandera | [CDH00] | Julia Juz | Thomas Noll |
| 12 | 21.01.02 | Java PathFinder | [HP98, VHB00] | Nils Wilhelms | Martin Leucker |
| 13 | 28.01.02 | Verifikation verteilter Java-Programme | [SL01] | Ansgar Pruene | Benedikt Bollig |
| 14 | 04.02.02 | Bytecode-Verifikation | [BFP99] | Sven Lukas | Martin Leucker |
Literatur
- [PVY99]
- D. Peled, M.Y. Vardi, M. Yannakakis: Black Box Checking, Proc. FORTE/PSTV, Kluwer, 1999, 225-240
- [FS01]
- B. Finkbeiner, H. Sipma: Checking Finite Traces Using Alternating Automata, Proc. CAV'01 Workshop on Runtime Verification, 2001
- [DDP99]
- S. Das, D.L. Dill, S. Park: Experience with Predicate Abstraction, Proc. CAV'99, LNCS 1633, Springer-Verlag, 1999, 160-171
- [SS99]
- H. Saidi, N. Shankar: Abstract and Model Check while you Prove, Proc. CAV'99, LNCS 1633, Springer-Verlag, 1999, 443-454
- [Tip95]
- F. Tip: A Survey of Program Slicing Techniques, Journal of Programming Languages 3(3), 1995, 121-189
- [HS99]
- G.J. Holzmann, M.H. Smith: Software Model Checking: Extracting Verification Models from Source Code, Journal on Formal Methods for Protocol Engineering and Distributed Systems, Kluwer, 1999, 481-497
- [LGS95]
- C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem: Property Preserving Abstractions for the Verification of Concurrent Systems, Formal Methods in System Design: An International Journal 6(1), Kluwer, 1995, 11-44
- [BMM01]
- T. Ball, R. Majumdar, T. Millstein, S.K. Rajamani: Automatic Predicate Abstraction of C Programs, Proc. PLDI'01
- [BPR01]
- T. Ball, A. Podelski, S.K. Rajamani: Boolean and Cartesian Abstraction for Model Checking C Programs, Proc. TACAS'01, LNCS 2031, Springer, 2001, 268-283
- [BR01]
- T. Ball, K. Rajamani: Automatically Validating Temporal Safety Properties of Interfaces, Proc. 8th SPIN Workshop, LNCS 2057, Springer-Verlag, 2001, 103-122
- [God97]
- P. Godefroit: Model Checking for Programming Languages Using VeriSoft, Proc. POPL'97, ACM Press, 1997, 174-186
- [Hol01]
- L. Holenderski: A Model Checking Project at Philips Research, Proc. 8th SPIN Workshop, LNCS 2057, Springer-Verlag, 2001, 288-295
- [Huc99]
- F. Huch: Verification of Erlang Programs Using Abstract Interpretation and Model Checking, Proc. ICFP'99, ACM SIGPLAN Notices 34(9), 1999
- [CDH00]
- J. Corbett et al.: Bandera: Extracting Finite-State Models from Java Source Code, Proc. 22nd Int. Conf. on Software Engineering, IEEE, 2000, 439-448
- [HP98]
- K. Havelund, T. Pressburger: Model Checking Java Programs Using Java PathFinder, Int. Journal on Software Tools for Technology Transfer (STTT), 2(4), 1998
- [VHB00]
- W. Visser, K. Havelund, G. Brat, S. Park: Model Checking Programs, Proc. 15th Int. Conf. on Automated Software Engineering, IEEE, 2000
- [SL01]
- S.D. Stoller, Y.A. Liu: Transformations for Model Checking Distributed Java Programs, Proc. 8th SPIN Workshop, LNCS 2057, Springer-Verlag, 2001, 192-199
- [BFP99]
- D. Basin, S. Friedrich, J. Posegga, H. Vogt: Java Bytecode Verification by Model Checking, Proc. CAV'99, LNCS 1633, Springer-Verlag, 1999, 491-494
Thomas Noll, Letzte Änderung: 03.12.2001