Formal verification: a principled approach to make systems that do what they should. The course has two aspects:
- learning the practice of formal verification - how to use tools to construct verified software
- understanding the principles behind formal verification and the ways in which verification tools work
-
From Viktor Kuncak
Abstract Satisfiability Modulo Theories (SMT) solvers are a critical component of many formal methods applications, including for software verification and… -
From Viktor Kuncak
Abstract: Refinement types decorate the types of a programming language with logical predicates to allow rnore expressive type specifications. Originally,… -
From Viktor Kuncak
Programming languages researchers have developed many advanced tools that promise to greatly ease software engineering. Yet even conceptually simple tools are expensive…