| Time slot (lecture) | Tuesday at 9:20 - 10:50 a.m. |
| Time slot (exercise) | Thursday at 1:00 - 2:30 p.m. |
| Location | Faculty of Computer Science, TU Dresden |
| Room (lecture) | APB/E001/U |
| Room (exercise) | APB/E006/U |
@inproceedings{
max_typed_binders_rocqPL26,
title = "Scalable Type Inference for Intrinsically-Typed Binders",
author = "Max Kurze, Clément Pit-Claudel, Sebastian Ertel",
year = "2026",
booktitle = "Workshop on Rocq for Programming Languages"
}
@inproceedings{
carmine_wp_prisc26,
title = "WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification",
author = "Carmine Abate, Mohamed Elsheikh, Kleio Liotati, Frantisek Farka, Sebastian Ertel",
year = "2026",
booktitle = "10th Workshop on Principles of Secure Compilation"
}
@article{
kan_string_cpp26,
title = "Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis",
author = "Shuanglong Kan, Anthony Widjaja Lin",
year = "2026",
journal = "Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs",
pages = "279-293"
}
@article{
10.1145/3776667,
title = "Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation",
author = "Marcus Rossel, Rudi Schneider, Kœhler Thomas, Michel Steuwer, Andrés Goens",
year = "2026",
journal = "Proc. ACM Program. Lang.",
month = "January",
number = "POPL",
volume = "10"
}
@inproceedings{
plos_25_farka_et_al,
title = "Debug, Execute, Verify! Development-Verification Co-Design Made Practical",
author = "Frantisek Farka, Carmine Abate, Shuanglong Kan, Sebastian Ertel",
year = "2025",
booktitle = "Proceedings of the 13th Workshop on Programming Languages and Operating Systems",
address = "New York, NY, USA",
series = "PLOS '25",
publisher = "Association for Computing Machinery",
pages = "51-59"
}
@inproceedings{
remote_attestation_ssprove_2026,
title = "Formally-verified Security against Forgery of Remote Attestation using SSProve",
author = "Sara Zain, Jannik Mähn, Stefan Köpsell, Sebastian Ertel",
year = "2025",
booktitle = "Computer Security — ESORICS",
publisher = "Springer Nature Switzerland",
pages = "463--484"
}
@article{
slotted_egraphs_2025,
title = "Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs",
author = "Rudi Schneider, Marcus Rossel, Kœhler Thomas, Andrés Goens, Michel Steuwer",
year = "2025",
journal = "Proceedings of the ACM on Programming Languages",
booktitle = "Proceedings of the ACM on Programming Languages",
address = "New York, NY, USA",
month = "jun",
number = "PLDI",
volume = "9",
publisher = "Association for Computing Machinery",
pages = "1888--1910"
}
@mastersthesis{
max_kurze_msc_thesis,
title = "A Framework for Modular and Compositional Reasoning in Kôika",
author = "Max Kurze",
year = "2025",
school = "Technische Universität Dresden",
month = "March",
url = "https://zenodo.org/records/15073479"
}
@mastersthesis{
garvit_chabra_msc_thesis,
title = "A formally-verified Network-on-Chip in Coq",
author = "Garvit Chhabra",
year = "2025",
school = "Technische Universität Dresden",
month = "January",
url = "https://zenodo.org/records/15004685"
}
@inproceedings{
ertelCOQ2024,
title = "On the Potential of Coq as the Platform of Choice for Hardware Design",
author = "Sebastian Ertel, Max Kurze, Michael Raitza",
year = "2024",
booktitle = "Coq Workshop",
url = "https://coq-workshop.gitlab.io/2024/files/EA4.pdf"
}
| 21.9.2023 | Dear students, The website for the Winter semester 2023/24 is now online. Please find all necessary information here. Our first lecture is on the 10th of October, 2023. Looking forward to see you there! |
Enter your username and password here in order to log in on the website