Docentship lecture: Interactive Formal Verification
- Date
- 14 February 2024, 13:15–14:15
- Location
- Ångström Laboratory, Ång 101127
- Type
- Lecture
- Lecturer
- Dr. Tjark Weber
- Organiser
- Institutionen för informationsteknologi
- Contact person
- Pierre Flener
The Department of Information Technology hereby invite all interested to a docentship lecture in subject computer science.
- Chairperson: professor Pierre Flener
- Representative of the Docentship Committee: professor Natasa Sladoje
Abstract: Formal methods allow to establish the correctness of hardware and software systems with mathematical rigor. The lecture will introduce attendees to interactive formal verification, a verification technique that involves utilizing a specialized computer program—a proof assistant—to construct formal proofs. The user interacts with the proof assistant by entering statements and providing reasoning steps; the assistant checks these for correctness. The lecture covers essential aspects such as interactive proof development, key features of proof assistants, and the application of formal reasoning to an imperative programming language. Moreover, it sheds light on current research challenges, and concludes with a discussion on the strengths and weaknesses inherent in interactive formal verification.
The lecture is an obligatory teaching test for those applying for admittance as docent and it should be possible for students and others with basic academic education in the relevant field to follow it. The lecture lasts 40-45 minutes with subsequent discussion. The lecture will be given in English.
Welcome!