Media and News

In the coming winter term, we will be offering the seminar Neural Networks in Formal Verification: Website (incl. registration link)

This seminar aims to provide an overview of the current research landscape in formal verification and the scope of neural networks in this domain. Specifically, it will explore two key aspects:

1. (1) Verification of Neural Networks (techniques, methods, and tools to ensure that neural networks operate safely, reliably, and as intended)

2. (2) Neural Networks for Verification (utilizing AI and machine learning techniques to enhance traditional verification methods)

We will be offering various seminar topics on both research directions (list currently still incomplete, please let us know if you are interested but looking for a different topic). If you want to participate in the seminar please register via the WiWi-Portal. The seminar will be in English.

More information ...

How can a voting system guarantee that the voter's vote remains undistorted? How secure are online voting systems and what are their limits? In their presentations on August 29, 2024, Felix Dörre and Michael Kirsten will examine computer-aided approaches that help to secure the integrity and confidentiality of the (online) voting process.

The talk “What are secure elections?” is an accompanying event to the current exhibition “Digiloglounge N°3. But is it secure?”. Currently on display there is “The Ignorant Voting Machine”, which was developed by Felix Dörre with the Cryptography and Security working group. Michael Kirsten and Felix Dörre provide an insight into the background to the associated research projects and invite you to a discussion.

The event starts at 6:30 pm. You will also have the opportunity to visit the exhibition “Digiloglounge N°3. But is it safe?” at 6 pm free of charge with the speakers and try out “The Ignorant Voting Machine” for yourself.

More information ...

Interested in doing research in formal methods? We are hiring!

Learn more ...

Mihai Herda very successfully defended his PhD on 2019-12-13. His dissertation is on "Combining Static and Dynamic Program Analysis Techniques for Checking Relational Properties".

Cordial congratulations from all his colleagues!

Am 29./30.11.2019 findet an unserem Lehrstuhl das 15. Treffen der GI-Gruppe FoMSESS (Formale Methoden und Software Engineering für sichere Systeme) statt. Das Treffen soll dem Austausch auf dem Forschungsgebiet dienen und insbesondere Nachwuchswissenschaftlern die Möglichkeit geben, ihre Arbeiten in einem informellen Rahmen vorzustellen.

In a new teaching laboratory, tools and programs are being developed for computer science teaching - developers orient themselves directly towards the needs of pupils and teachers.

In order to master the challenges of digitization as adults, pupils need a broad basic education in computer science. However, teachers often lack the right tools to teach subjects such as software development or IT security. In the new open-source teaching software laboratory at the Karlsruhe Institute of Technology (KIT), students will gain practical experience in the development of open-source software and at the same time develop materials for teaching computer science.

Read more ...

Sarah Grebing very successfully defended her PhD on 2019-02-07. Her dissertation is on "User Interaction in Deductive Interactive Program Verification".

Cordial congratulations from all her colleagues!

Also this summer term, we offer a project as part of the bachelor course "Software Engineering Practice". On May 4, 2018, the project of summer term 2018 on the topic "Blockchain-based E-Voting" started. Within this project, a team of five bachelor students develops a complete software project according to the state of the art in software engineering. This semester, we use the permissioned Blockchain technology Hyperledger Fabric to realize traceable electronic elections by using a distributed ledger.

We offer a wide range of new topics for master and bachelor theses in areas such as verification of PLCs, extension of the KeY verification approach, formalisation/verification of social choice properties, and much more. Besides the advertised topics, we are open to your ideas within our research fields. If you are interested, please contact the respective members of our group.

Topics and Research Fields for Student Theses

The new book covers deductive software verification as realised by the KeY approach. It constitutes the ultimate source for the KeY tool since version 2.6.

The KeY book is published by Springer as vol. 10001 in the LNCS series) and available at Springer Link.

More information

CVE-2016-6313 - Critical bug in the GnuPG/Libgcrypt PRNG found with the help of the Entroposcope tool, developed by Felix Dörre and Dr. Vladimir Klebanov as part of the DeduSec project within the RS³ priority programme. The paper describing how Entroposcope works was presented at ACM CCS 2016 in Vienna in October 2016.

Update: Presentation at the 33th Chaos Communication Congress (33C3)