Bachelorseminar: Software Verification: Tools and Techniques

Beschreibung

Abstract

The everlasting burden of debugging strains developers nerves and industries budgets.
Testing aims to remedy software bugs but often fails to discover intricate failures.
This is where Software Verification enters the frame: Using abstractions and models generated from the
source code, Verification tools try to prove a program correct with respect to a specification; or witness a counterexample in case
the specification is violated.

In this Seminar you will learn more about tools used to verify programs and the techniques and algorithms behind them.

Organization

This seminar is accredited at 3 ECTS.
The language of communication is German or English.
Each student will be assigned one of the 15 proposed papers. You will learn to read and analyze the paper. Based on that you will
give a presentation on your topic and write a short report (8-10 pages LNCS format).
The report as well as the final presentation is expected to be in English.

Weekly Meetings

To guide you through the topic we will meet on a weekly basis. If possible the meetings will be in presence.
The weekly meetings will be used to discuss your progress, short intermediate presentations and short lectures and exercises on writing, plagiarism etc.

Prerequisites

  • Basic knowledge of algorithm notation
  • Basic knowledge about automata
  • Interest in Software Verification

Schedule

  • October 20, 2022: Organization & Overview
  • October 25, 2022: Submit your 3 favorite topics via Uni2Work
  • October 27, 2022: Assignment of topic and mentor + Tutorial: Report & Presentation
  • November 03, 2022: Intro to LaTeX (recommended) + Homework for correct citing
  • November 10, 2022: Discussion of homework + Tutorial: Reading Papers & Literature Research
  • November 17, 2022: Game (+ Q&A if time permits)
  • November 24, 2022: Lightning Talks (5 minutes + discussion)
  • December 01, 2022: Q&A: Your questions to the seminar (topic, presentation, report)
  • December 08, 2022: Reviews & Conferences & Publications & Artifacts
  • December 15, 2022: Recommended: Meet with your mentor
  • December 22, 2022: Recommended: Meet with your mentor
  • December 29, 2022: Christmas Holiday
  • January 05, 2023: Christmas Holiday
  • January 12, 2023: Recommended: Review drafts of your fellows
  • January 19, 2023: Recommended: Presentation dry runs
  • January 26, 2023: Submit report via Uni2Work (PDF, 50% of your grade)
  • January 28, 2023: Final Presentation (50% of your grade)

Requirements to pass

  • Presentation of ca. 20min
  • Written report of 8-10 Pages without references

Each student is responsible on their own to follow the rules of good scientific practice. Please ask mentors in case of a doubt. Plagiarism will lead to failing the seminar.

List of Topics

Paper Link
Combining Model Checking and Data-Flow Analysis (up to 16.4) https://doi.org/10.1007/978-3-319-10575-8_16
Witness validation and stepwise testification across software verifiers https://doi.org/10.1145/2786805.2786867
Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR https://doi.org/10.1145/3510003.3510064
CoVeriTeam: On-Demand Composition of Cooperative Verification Systems https://doi.org/10.1007/978-3-030-99524-9_31
Bounded model checking https://doi.org/10.1016/S0065-2458(03)58003-2
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs https://dl.acm.org/doi/10.5555/1855741.1855756
SMT-based Software Model Checking: An Experimental Comparison of Four Algorithms https://doi.org/10.1007/978-3-319-48869-1_14
Symbolic Execution and Program Testing https://doi.org/10.1145/360248.360252
BDD-Based Symbolic Model Checking https://doi.org/10.1007/978-3-319-10575-8_8
Software Model Checking for People Who Love Automata https://doi.org/10.1007/978-3-642-39799-8_2
Refinement of Trace Abstraction https://doi.org/10.1007/978-3-642-03237-0_7
Counterexample-Guided Abstraction Refinement https://doi.org/10.1007/10722167_15
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution https://doi.org/10.1007/978-3-642-32469-7_14
Boosting k-Induction with Continuously-Refined Invariants https://doi.org/10.1007/978-3-319-21690-4_42
Software model checking via large-block encoding https://doi.org/10.1109/FMCAD.2009.5351147
Separation logic: A logic for shared mutable data structures https://doi.org/10.1109/LICS.2002.1029817
Institut
Institut für Informatik
Dozent:in
Assistent:innen
Kursteilnehmer:innen
12 von 14
Zentralanmeldung
Bachelorseminare
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
NameAnmeldung abAnmeldung bisTerminPrüfungsanmeldung
Nicht zur Prüfung angemeldet
Termine
ArtZeitRegulärer RaumNotiz
Weekly Meeting
  • Do 10:15–11:45
Raum 033, Oettingenstr. 67