Bachelorseminar Softwarequalität

• Prüfungen
  • Seminarnote

Aktuelles

• Seminarplätze und potentielle Nachrücker

  An alle, die derzeit noch einen Seminarplatz suchen:

  Dieses Seminar ist voll und ich kann Ihnen derzeit keinen Platz anbieten. Es ist auch nicht wahrscheinlich, dass noch Plätze freiwerden.

  Falls Sie die Zentralanmeldung verpasst haben: am besten tragen Sie sich jetzt schon mal einen Eintrag im Kalender für das nächste Jahr ein. Ohne Teilnahme an der Zentralanmeldung bekommen Sie keinen Seminarplatz.

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

Beschreibung

In diesem Bachelorseminar werden wir unterschiedliche Techniken, Ansätze, Theorien, Fallstudien und Softwaretools zur Sicherung von Softwarequalität unter die Lupe nehmen. Die Studierenden führen eine Literaturrecherche zu ihren jeweilgen Themen durch, probieren Tools in praktischen Experimenten aus, und präsentieren die Einsichten und Ergebnisse in einer Videoaufzeichnung sowie einer schriftlichen Ausarbeitung.

Organisation

Das Seminar findet online statt, falls möglich treffen wir uns im Sommer persönlich zu einer Abschlussveranstaltung. Das Seminar findet auf deutsch statt, wir ermutigen Sie aber, ihre Präsentation und/oder auf englisch zu halten und eine kleine Anzahl von Themen wird ausschließlich in englisch angeboten.

Die Themen stellen die Mitarbeiter vom https://www.sosy-lab.org/, eine Liste veröffentlichen wir noch. Hier können Sie sich z.B. schon mal einen groben Eindruck verschaffen: https://uni2work.ifi.lmu.de/course/W20/IfI/QA

Inhalt und Zeitplan

• wir treffen uns einige mal virtuell, um verschiedene Themen zu besprechen (wie halte ich einen guten Vortrag, wie schreibe ich einen wissenschaftlichen Text)
• Abgabe der Präsentation als Videoaufzeichnung: vor dem Ende der Vorlesungszeit
• Abgabe der schriftlichen Ausarbeitung: August

Anforderungen

• Präsentation als Videoaufzeichnung (25min)
• 8-10 Seiten Ausarbeitung im LNCS Stil
• Besprechung der Präsentation sowie Ausarbeitung vor der Abgabe in je einem Meeting mit dem jeweiligen Betreuer
• Sie sind selbst verantwortlich, die Regeln der guten wissenschaftlichen Praxis sowie des korrekten Zitierens einzuhalten (besprechen wir im Detail, im Zweifelsfall einfach fragen)

Das Seminar gibt 3 ECTS Punkte.

Themen

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

   • A decade of software model checking with SLAM
     
   • DART: directed automated random testing
     
   • Also: Z3, Dafny, Everest, F*, Lean

3. Amazon AWS verified infrastructure (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 (Assigned)

   • Lessons from building static analysis tools at Google
   • Project Zero

5. Solving Satisfiability Problem by Quantum Computing (survey)

6. Learning Software Quality Assurance with Bricks (Martin) (Assigned)

   • https://ir.canterbury.ac.nz/bitstream/handle/10092/101650/2021_ICSE_SEET_SQA_and_LEGOs.pdf"]

7. A Tale from the Trenches: Cognitive Biases and Software Development (Martin) (Assigned)

   • https://par.nsf.gov/servlets/purl/10189093

8. Improving the Pull Requests Review Process Using Learning-to-rank Algorithms (Martin) (Assigned)

   • https://link.springer.com/article/10.1007%2Fs10664-019-09696-8

9. Speculative Analysis for Quality Assessment of Code Comments (Martin) (Assigned)

   • https://arxiv.org/abs/2102.09605

10. Function summaries/invariants from dynamic analyses (Thomas L)

    • 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)

11. EvoSuite (Thomas L) (Assigned)

    • Gordon Fraser, Andrea Arcuri: EvoSuite: automatic test suite generation for object-oriented software. SIGSOFT FSE 2011: 416-419

12. Function summaries/invariants from machine learning (survey, Thomas) (Thomas L)

    • 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

13. Verifying OpenJDK’s LinkedList using KeY (Philipp)

    • https://link.springer.com/chapter/10.1007%2F978-3-030-45237-7_13

14. An Empirical Study on the Use and Misuse of Java 8 Streams (Philipp) (Assigned)

    • https://link.springer.com/chapter/10.1007%2F978-3-030-45234-6_5

15. MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers (Philipp)

    • https://link.springer.com/chapter/10.1007%2F978-3-030-72013-1_16

16. FlowType (Sudeep) (English) (Assigned)

    • https://flowtype.org
    • https://dl.acm.org/doi/pdf/10.1145/3290329

17. TypeScript (Sudeep) (English) (Assigned)

    • http://typescriptlang.org
    • https://dl.acm.org/doi/pdf/10.1145/3290329

18. Collective Knowledge (Sudeep) (English) (Assigned)

    • https://cknowledge.org
    • http://tomgruber.org/writing/CollectiveKnowledgeSystems.pdf

19. Program Repair - GenProg (Sudeep) (English) (Assigned)

    • https://squareslab.github.io/genprog-code/

20. Program Repair - Clara (Sudeep) (English)

    • https://github.com/iradicek/clara

21. The Program Verifier Dafny (Gidon) (Assigned)

    • https://github.com/dafny-lang/dafny

22. Liquid Types in Haskell (Gidon) (Assigned)

    • LiquidHaskell: Experience with Refinement Types in the Real World

23. Systemmodellierung und Refinement mit Event-B (Gidon) (Assigned)

    • Abrial: Modeling in Event-B: system and software engineering
    • Abrial et al: Rodin: an open toolset for modelling and reasoning in Event-B

24. Taint Analysis for Android
    - Pauck et al: Do android taint analysis tools keep their promises?
    - Huang et al: Scalable and precise taint analysis for android

25. Rust, mit Fokus auf Ownership (Assigned)

26. Scala, mit Fokus auf Integration OOP und funktionale Programmierung (Assigned)

27. The Program Verifier Why3 (Gidon)

    • http://toccata.lri.fr/gallery/why3.en.html

28. Verified Programming in Agda oder Lean mit dependent types (Gidon)

29. Testing and debugging quantum programs

    • https://dl.acm.org/doi/10.1145/3428218
    • https://dl.acm.org/doi/abs/10.1145/3307650.3322213

Institut

Institut für Informatik

Dozierende

• Gidon Ernst
• Sudeep Kanav
• Philipp Wendler

Kursteilnehmer:innen

19 von 22

Zentralanmeldung

Bachelorseminare

Anweisungen zur Bewerbung

Bitte schreiben Sie uns ein oder zwei Sätze, warum Sie dieses Thema interessiert, und falls vorhanden, auch Ihre Vorerfahrungen

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
Seminarnote				Nicht zur Prüfung angemeldet