Comparing Deductive Program Verification of Graph Data Structures
| Forschungsthema: | KeY |
|---|---|
| Typ: | BA |
| Datum: | 2018-06-04 |
| Betreuer: |
Michael Kirsten Mattias Ulbrich |
| Aushang: |
Content
These days, graphs and graph-based algorithms are ubiquitous. They appear as social network graphs, syntax trees of formal languages or represent traffic networks. Depth first-search (DFS) is a simple algorithm for traversing graphs, which marks the thereby visited nodes of the graph. Many graph algorithms, e.g., Dijkstra‘s algorithm for finding shortest paths or Tarjan‘s algorithm for computing strongly connected components, are based on DFS. So, despite its simplicity, DFS has some importance. Moreover, especially for efficient implementations of such graph algorithms, graphs can be represented by a variety of data structures, some may be easier to understand or implement, others maybe better regarding efficiency with respect to run-time or memory usage.
Within this thesis, we would like to verify common implementations of such graph algorithms using different graph representations and compare their differences or commonalities regarding their suitability for the verification process using the programm verification system KeY. KeY is jointly developed in our group together with groups at TU Darmstadt and Chalmers University of Technology (Gothenburg, Sweden).
Requirements
- Knowledge as taught in the lecture 'Formale Systeme' is helpful
Supervision and contact
- Dr. Mattias Ulbrich (Room 229, Geb. 50.34)
- Michael Kirsten (Room 228, Geb. 50.34)