Research at Work 2023: “Generalized Equivalence Checking” (MTV TU Berlin)

# Research at Work 2023: “Generalized Equivalence Checking” (MTV TU Berlin) This year's RaW projects will be all about **characterizing and checking behavioral equivalences** (bisimilarity, trace equivalence, etc) using a nice game-theoretic framework. The topic connects to a wide range of exciting research areas such as program semantics, concurrency theory, model checking, graph algorithms, quantitative games, and modal logics. :::info If you want to participate, please sign up for the [ISIS course](https://isis.tu-berlin.de/course/view.php?id=35278) and write an email to benjamin.bisping@tu-berlin.de by 2023-10-13 outlining your background in concurrency theory and formal methods. ::: ## Format - Project work with 2–4 groups of 2–4 students - Produce something to show the academic world (Isabelle/HOL proofs, verification tools, papers) - 9 credit points, MSc Computer Science (or MSc Computer Engineering) - Start: Mo, 2023-10-16, 10:15, TEL 512 Physical meetings every Monday 10–12 and Thursday 14–16 in TEL 512. - Contact: [Benjamin Bisping](https://bbisping.de) / benjamin.bisping@tu-berlin.de ## Tasks and Skills Depending on the participants' backgrounds and preferences, the groups will be formed around tasks like the following ones: - Isabelle/HOL formalizations of - behavioral equivalences - energy games / [multi-weighted reachability games](https://arxiv.org/abs/2308.09625), and - the “[spectroscopy game](https://doi.org/10.1007/978-3-031-37706-8_5).” - Corresponding code for tool support. (Requires skills with web technologies / Scala / TypeScript / C++, depending on participants.) ## Material - [ISIS course](https://isis.tu-berlin.de/course/view.php?id=35278) - Module decription: [MTV Project: Research at Work](https://moseskonto.tu-berlin.de/moses/modultransfersystem/bolognamodule/beschreibung/anzeigen.html?nummer=40766&version=6&sprache=2) - CAV'23 paper: [Process Equivalence Problems as Energy Games](https://doi.org/10.1007/978-3-031-37706-8_5) - Draft paper: [Linear-Time–Branching-Time Spectroscopy Accounting for Silent Steps](https://doi.org/10.48550/arXiv.2305.17671)