Du är inte inloggad på KTH så innehållet är inte anpassat efter dina val.
Kurswebben har varit stängt för redigering sedan första juni 2025 och kommer stängas ned helt första oktober 2026. Utifrån hur kurswebben har använts finns det några olika alternativ för ersättare:
Är du intresserad av mer information om detta, kontakta e-learning@kth.se.
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.