Software Quality Assurance

Beschreibung

This seminar introduces the students to different aspects of software quality assurance (QA): state of the art techniques, tools, case studies, challenges and opportunities.
Students will have to give a presentation about a topic and write a report.

The seminar will be held online.

Preliminary Schedule (dates subject to poll results)

The seminar will take place on ZOOM (link will be distributed)..

Nov 11: Introduction of the topic; organizational matters (presented by the organizers)
Nov 18: Group discussions: criteria for good presentations and good written reports; distribution of topics. Homework: record a two mins, 1 slide presentation on the topic
Nov 25: We watch all two mins presentations together and discuss
Dec 2: (maybe): academic writing, literature research (presented by the organizers)

After the winter break (deadlines & dates to be decided)

  • each participant submits the recording of the full talk
  • each participant prepares a question for her/his own video
  • each participant watches a few (2-4) videos and provides: 1) answer to the respective question + a few notes on 2) what was great about the presentation 3) what could be improved

At the end of the semester, we meet again for a final round of discussion (feedback on the organization of the seminar will be appreciated then)

Finally, the written report is due (deadline to be decided)

Requirements

The students are expected to:

Language

The seminar will be conducted in English.
Students are expected to discuss with their mentors, write the reports and give the presentations in English.

Topics

Goals/Criteria:

  • do your own literature review!
  • introduce project, technique, tool, or field
  • clearly state: what is the problem being addressed?
  • use illustrative examples
  • expose key achievements
  • explain relevance in broader context
  • discuss theoretical contributions
  • discuss potential practical use as well as limitations

Overview

  1. Starting point:

Quality Assurance in the Real World

  1. seL4 Kernel: the world’s first fully verified operating system kernel
    • 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, Gidon)
    • 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, Gidon)
    • 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, Gidon)
    • Lessons from building static analysis tools at Google
    • Project Zero
  5. Formal methods at Facebook (survey/practical, Gidon)
    • Moving Fast with Software Verification
    • Scaling static analyses at Facebook
    • Continuous reasoning: Scaling the impact of formal methods
    • From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis
  6. Akita Software API documentation (Gidon)
    • Yang, Jean: How APIs Are Both the Illness and the Cure: The Software Heterogeneity Problem in Modern Web Applications
    • https://www.akitasoftware.com/

Software Testing/Fuzzing

  1. Fuzzing SMT solvers (survey/practical, already assigned, Gidon)
    • Fuzzing and delta-debugging SMT solvers
    • Stringfuzz: A fuzzer for string solvers
    • BanditFuzz: Fuzzing SMT Solvers with Reinforcement Learning
    • Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing
  2. Property based random testing (survey/practical, Gidon)
    • Fink, George, and Matt Bishop. Property-based testing: a new approach to testing for assurance.
  3. MAGMA ground truth fuzzing benchmark set (practical, Gidon)
  4. Runtime verification (survey, Sudeep)

Overview of techniques in an area

  1. Automatic program repair (survey, Sudeep)
  2. Fault localization (survey, Sudeep)
  3. SeaHorn verification framework (practical, Sudeep)
  4. Crab (CoRnucopia of ABstractions) (practical, Sudeep)
  5. Program synthesis (survey/practical, Gidon or Sudeep)
  6. Function summaries from formal analyses (survey, Thomas)
  7. Function summaries/invariants from dynamic analyses (survey, Thomas)
    • Earl T. Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, Shin Yoo: The Oracle Problem in Software Testing: A Survey. IEEE Trans. Software Eng. 41(5): 507-525 (2015)
    • Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, Chen Xiao: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3): 35-45 (2007)
    • Gordon Fraser, Andrea Arcuri: EvoSuite: automatic test suite generation for object-oriented software. SIGSOFT FSE 2011: 416-419][Fraser2011]
  8. Function summaries/invariants from machine learning (survey, Thomas)
    • Seyed Reza Shahamiri, Wan Mohd Nasir Wan-Kadir, Suhaimi Ibrahim, Siti Zaiton Mohd Hashim: An automated framework for software test oracle. Inf. Softw. Technol. 53(7): 774-788 (2011)
    • Facundo Molina, Renzo Degiovanni, Pablo Ponzio, Germán Regis, Nazareno Aguirre, Marcelo F. Frias: Training binary classifiers as data structure invariants. ICSE 2019: 759-770
Institut
Institut für Informatik
Dozierende
Kursteilnehmer:innen
13 von 20
Zentralanmeldung
Hauptseminare (Master)
Anweisungen zur Bewerbung

Please submit a short statement of motivation, in English, for your participation in this seminar (5-10 sentences). You might refer to both your interest as well as your prior experience with the topic of the seminar.

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
NameNameAnmeldung abAnmeldung abAnmeldung bisAnmeldung bisTerminTerminPrüfungsanmeldungPrüfungsanmeldung
Seminar Grade
Nicht zur Prüfung angemeldet
Termine
ArtArtZeitZeitRegulärer RaumRegulärer RaumNotizNotiz
Seminar
  • Mi 10:15–12:00
Zoom