Du är inte inloggad på KTH så innehållet är inte anpassat efter dina val.
Från och med den 1 juni 2025 upphör möjligheten att redigera innehåll i kurswebben och studenter slutar bli inlagda. Redan existerande material kvarstår.
Läs mer här: Kurswebbens solnedgång den första juni
As software systems become more complex, ensuring that they adhere to given requirements for safety and reliability becomes more difficult. At the same time, individuals, organisations, and societies increasingly depend on such complex systems. Interactive theorem provers (ITPs) are powerful, flexible, and reliable tools for system modeling and formal verification. A growing use of ITPs is for specification and construction of practical and trustworthy large-scale software systems. This course gives an overview of the foundations and technologies for ITPs and how they can be applied to model, specify, and formally verify software systems, including both abstract system models and executable programs.