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
Name Anmeldung ab Anmeldung bis Termin Prüfungsanmeldung Nicht zur Prüfung angemeldet- Termine
Art Zeit Regulärer Raum Notiz Weekly MeetingRaum 033, Oettingenstr. 67