MA-INF 3318 - Seminar Verification of Complex Systems, Winter Term 2013/14

For the instalment of this course in Winter Term 2015/16, see here.

Lecturers:

• Dr. Michael Gerz (FKIE)
• Dr. Marc Spielmann (FKIE)
• Jun.-Prof. Dr. Janis Voigtländer (Uni Bonn)

Organizational Notes:

• The seminar belongs to the track Information and Communication Management of the Master Programme.
• Weekly meetings (when taking place) will be on Mondays, 12:15-13:45, in Römerstr. 164, room A121.
• The assignment of topics to students is now listed in eCampus: https://ecampus.uni-bonn.de/goto_ecampus_crs_340103.html

About the Seminar:

The seminar is jointly organized by researchers from the Fraunhofer-Institut für Kommunikation, Informationsverarbeitung und Ergonomie (FKIE) and the University of Bonn. The focus is on techniques for analyzing the correctness of complex systems such as software. Both theoretical foundations for such techniques and consideration of practical tools are of interest. Specific themes of interest include (a selection will be made, see literature and tools below):

1. Specification formalisms and languages
2. Decision problems
3. Modelling desired properties of a system
4. Model checking
5. Theorem proving
6. Static (flow) analysis, abstract interpretation
7. Code analysis using heuristics
8. Testing (approaches, frameworks, coverage criteria)
9. Runtime verification (instrumentation, monitoring)
10. Applications and pragmatics of verification

The aim of the seminar is that students develop profound knowledge about a given subject by studying the literature, understanding scientific publications, presenting the results in written and oral form, and discussing with fellow students. Each student (max. 10) will be given literature on an assigned topic, will read that and possibly further literature selected on their own, and after self-study and discussion with a supervisor (from among the lecturers) will write a seminar essay on the topic (about 10 pages). In addition, each student will give a talk on the assigned topic (about 40 minutes, plus discussion). Both the essay and the talk will be graded.

Prerequisites:

The seminar does not depend on a specific previous lecture. A general command of logic and mathematical formalisms is expected.

Literature and Tools:

In Winter Term 2013/14, the following literature and tools will be considered (one or more per participant):

• TTCN-3, Testing and Test Control Notation 3, http://www.ttcn-3.org/
  (theme 1. from above)
• Model-Driven Testing with the UML Testing Profile, http://utp.omg.org/
  (theme 1. from above)
• E.A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed., vol. B., Elsevier Science Publishers, 1990, 995-1072.
  (themes 1. and 2. from above)
• M. Prasad, A. Biere, and A. Gupta. A survey of recent advances in SAT-based formal verification. Int J Softw Tools Technol Transfer (2005) 7: 156-173.
  (theme 2. from above)
• A. Biere, A. Cimatti, E.M. Clarke, and Yunshan Yhu. Symbolic model checking without BDDs. In: TACAS (1999), 193-207.
  (theme 4. from above)
• E.M. Clarke, D. Kroening, and F. Lerda: A Tool for Checking ANSI-C Programs. In: TACAS (2004), 168-176.
  (theme 4. from above)
• CBMC, A Bounded Model Checker for ANSI-C and C++ programs, http://www.cs.cmu.edu/~modelcheck/cbmc/
  (theme 4. from above)
• D. Hovemeyer, W. Pugh: Finding Bugs is Easy. ACM SIGPLAN Notices, Volume 39, Issue 12, 2004, 92-106.
  (theme 6. from above)
• N. Rutar, C.B. Almazan, J.S. Foster: A Comparison of Bug Finding Tools for Java. In: ISSRE (2004), IEEE Computer Society, 245-256.
  (theme 6. from above)
• A. Holzer, Ch. Schallhart, M. Tautschnig, and H. Veith. Query-driven program testing. In: VMCAI (2009), Springer, volume 5403 of Lecture Notes in Computer Science, 151-166.
  (theme 8. from above)
• M. Tautschnig. Query-Driven Program Testing. PhD thesis, Vienna University of Technology, 2011.
  (theme 8. from above)
• FShell, A testing environment for C programs, http://forsyte.at/software/fshell/
  (theme 8. from above)
• W. Visser, K. Havelund, G. Brat, S.-J. Park, and F. Lerda. Model Checking Programs. Automated Software Engineering Journal, 10(2), 2003.
  (theme 8. from above)
• Java PathFinder, http://babelfish.arc.nasa.gov/trac/jpf/wiki/WikiStart
  (theme 8. from above)
• M. Veanes, C. Campbell, W. Grieskamp, W. Schulte, N. Tillmann, and L. Nachmanson. Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. Lecture Notes in Computer Science, 2008, volume 4949, 39-76.
  (theme 8. from above)
• M. Goedicke, T. Menzies, S. Motoshi. Communicating continuous integration servers for increasing effectiveness of automated testing. In: ASE (2012), ACM, 374-377.
  (theme 8. from above)
• S. Stolberg. Enabling Agile Testing through Continuous Integration. In: AGILE (2009), 369-374.
  (theme 8. from above)
• R.A. Razak, F.R. Fahrurazi: Agile testing with Selenium. In: Proceedings of the 2011 Malaysian Conference in Software Engineering, IEEE, 2011, 217-219.
  (theme 8. from above)
• T. Rings, J. Grabowski, S. Schulz. On the Standardization of a Testing Framework for Application Deployment on Grid and Cloud Infrastructures. In: VALID (2010), 99-107.
  (theme 8. from above)
• The DSL-based Spock test framework, http://code.google.com/p/spock/
  (theme 8. from above)
• N. Nethercote, J. Seward: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI (2007), ACM, 89-100.
  (theme 9. from above)

Site proudly generated by Hakyll; Page changed October 2013