Software Quality Assurance (Master Seminar)

• Prüfungen
  • Seminar Grade

Aktuelles

• Information for students seeking a seminar seat

  This seminar is full and it is unlikely that seats become free again, apologies. Note, as a docent I have little influence over how the seats are distributed by Uni2Work.

  Please keep in mind to register for “Zentralanmeldung” next semester if you missed it this time, best put a note in your calendar already.

  Zuletzt verändert: Do 15 Apr 2021 11:00

Beschreibung

Topic

This master seminar introduces the students to different aspects of software quality assurance (QA): state of the art techniques, tools, case studies, challenges and opportunities. Participants will review scientific literature, experiment with tools (where available) to understand the details of the assigned topic, and present it to others in a clear way, using their own words.

Organization: The seminar will be held (mostly) online, with a meeting in person at the end if possible.

The seminar will be held in English, including the introduction and discussions, but selected topics are available in German.

Content and Schedule (exact deadlines to be decided)

• we will virtually meet a couple of times as a group to discuss aspects of good presentations and good writing, how to conduct literature research, and so on
• before the end of the teaching period, each participant prepares and submits a video recording of their presentation
• after the end of the teaching period, everybody submits their written report (roughly: August)

Requirements

• give a presentation of 25 minutes including a practical demo if possible
• submit a report of approx. 10-12 pages, style: LNCS
• both the presentation and the report must be discussed with your advisor in advance to submission
• participants are responsible for themselves to adhere to rules of proper scientific conduct and adequate citations (we will discuss what that means and you can always ask)

All requirements are strict and each one must be satisfied to pass the seminar.
The seminar will give 6 ECTS points.

Topics

Quality Assurance in the Real World

1. seL4 Kernel: the world’s first fully verified operating system kernel (Assigned)
   • Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood:
     seL4 - formal verification of an OS kernel
   • Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein:
     seL4 - From General Purpose to a Proof of Information Flow Enforcement.
2. Formal methods at Microsoft (survey/practical)
   • A decade of software model checking with SLAM
     
   • DART: directed automated random testing
     
   • Also: Z3, Dafny, Everest, F*, Lean
3. Amazon AWS verified infrastructure (survey) (Assigned)
   • Continuous formal verification of Amazon s2n
   • How Amazon web services uses formal methods
   • Stratified abstraction of access control policies
   • Reachability analysis for AWS-based networks
4. Formal methods at Google (survey) (Assigned)
   • Lessons from building static analysis tools at Google
   • Project Zero

Software Testing/Fuzzing

5. Property based random testing (survey/practical) (Assigned)
   • Fink, George, and Matt Bishop. Property-based testing: a new approach to testing for assurance.
6. MAGMA ground truth fuzzing benchmark set (practical) (Assigned)
   • Hazimeh, Ahmad, Adrian Herrera, and Mathias Payer. Magma: A Ground-Truth Fuzzing Benchmark
   • https://hexhive.epfl.ch/magma/
7. Vasudev Vikram, Rohan Padhye, Koushik Sen: Growing a Test Corpus with Bonsai Fuzzing, ICSE 2021, https://arxiv.org/abs/2103.04388

Verification tools / frameworks

8. SeaHorn verification framework
   • The SeaHorn Verification Framework
     Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A.Navas
     https://doi.org/10.1007/978-3-319-21690-4_20
   • http://seahorn.github.io/
9. Infer (Assigned)
   • https://fbinfer.com/
10. Nitwit (Assigned)
    • https://link.springer.com/chapter/10.1007/978-3-030-45190-5_3
11. LLVM
    • https://llvm.org/
    • https://llvm.org/pubs/2004-01-30-CGO-LLVM.html

Theorem Provers

12. Coq proof assistant
    - https://coq.inria.fr/

13. LEAN

    • https://leanprover.github.io/

14. Boogie - language and tool

    • https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/

Overview of techniques in an area

15. Automatic program repair (survey) (Assigned)
    • Automatic Software Repair: A Survey
      Luca Gazzola, Daniela Micucci, and Leonardo Mariani
      https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=8089448
    • Automatic Software Repair: a Bibliography
      Martin Monperrus
      https://dl.acm.org/doi/abs/10.1145/3105906
      https://arxiv.org/pdf/1807.00515.pdf
16. Fault localization (survey) (Assigned)
    • A survey on software fault localization
      W Eric Wong, Ruizhi Gao, Yihao Li , Rui Abreu, Franz Wotawa
      https://ieeexplore.ieee.org/document/7390282
17. Program synthesis (survey/practical)
    • Allamanis, Miltiadis, et al.: Mining semantic loop idioms, https://discovery.ucl.ac.uk/id/eprint/10062734/1/Barr_coils.pdf
    • Shin, Eui Chul, et al: Program Synthesis and Semantic Parsing with Learned Code Idioms, https://papers.nips.cc/paper/9265-program-synthesis-and-semantic-parsing-with-learned-code-idioms.pdf
    • Alur et al: Syntax Guided Synthesis
    • Possible directions via tools: Synquid, Liquid Haskell, Leon, Lifty
    • Sumit Gulwani, Oleksandr Polozov, Rishabh Singh
      https://www.microsoft.com/en-us/research/wp-content/uploads/2017/10/program_synthesis_now.pdf
18. Function summaries from formal analyses (survey)
    • Patrice Godefroid: Compositional dynamic test generation. POPL 2007: 47-54
    • Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina: Function Summarization-Based Bounded Model Checking. Validation of Evolving Software 2015: 37-53
    • Sery2015: https://link.springer.com/chapter/10.1007/978-3-319-10623-6_5

Institut

Institut für Informatik

Dozierende

• Gidon Ernst
• Sudeep Kanav

Kursteilnehmer:innen

12 von 13

Zentralanmeldung

Hauptseminare (Master)

Anweisungen zur Bewerbung

Please write one or two sentences about why you are interested in the topic of software quality assurance, and if applicable mention your prior knowledge or experience with this topic.

Material

Das Kursmaterial ist nur für Mitglieder des Kurses einsehbar, also z.B. für Teilnehmer:innen, Tutor:innen, Korrektor:innen und Verwalter:innen.

Prüfungen

Name	Anmeldung ab	Anmeldung bis	Termin	Prüfungsanmeldung
Seminar Grade				Nicht zur Prüfung angemeldet