Docenturföreläsning: Interactive Formal Verification
- Datum: 14 februari 2024, kl. 13.15–14.15
- Plats: Ångströmlaboratoriet, Ång 101127
- Typ: Föreläsning
- Föreläsare: Dr. Tjark Weber
- Arrangör: Institutionen för informationsteknologi
- Kontaktperson: Pierre Flener
Institutionen för informationsteknologi inbjuder härmed alla intresserade till docenturföreläsning i ämnet datalogi.
- Ordförande:professor Pierre Flener
- Docenturnämndens representant: professor Natasa Sladoje
Sammanfattning (på engelska): 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.
Föreläsningen, som är ett lärarprov för den som ansökt om att bli antagen som docent, ska kunna följas av studenter och andra med kunskaper på grundutbildningsnivå inom ämnet, men kan även vara av intresse för en bredare publik. Föreläsningen varar 40-45 minuter med efterföljande diskussion och kommer att ges på engelska.
Välkomna!