Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Introduction to Formal Verification

Description

This lecture introduces the principles and practice of formal verification, focusing on constructing verified software using tools and understanding the underlying principles. The course emphasizes the rigorous proof that computer systems satisfy specifications, contrasting formal verification with testing. It covers topics such as automated theorem proving, compiling programs to formulas, and the importance of mathematical models in ensuring system correctness.

Official source

Related concepts (32)

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Software verification and validation

In software project management, software testing, and software engineering, verification and validation (V&V) is the process of checking that a software system meets specifications and requirements so that it fulfills its intended purpose. It may also be referred to as software quality control. It is normally the responsibility of software testers as part of the software development lifecycle.

Formal methods

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Formal specification

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

Software testing

Software testing is the act of examining the artifacts and the behavior of the software under test by validation and verification. Software testing can also provide an objective, independent view of the software to allow the business to appreciate and understand the risks of software implementation. Test techniques include, but are not necessarily limited to: analyzing the product requirements for completeness and correctness in various contexts like industry perspective, business perspective, feasibility and viability of implementation, usability, performance, security, infrastructure considerations, etc.

Related lectures (35)

Automated Testing: Fuzzing and Sanitization

Explores fuzzing, bug oracles, code reviews, and automated testing techniques, emphasizing the importance of sanitization in detecting faults.

Correctness of Compilers: Part 1

Explores compiler correctness, examples of verified compilers, formal verification, and the challenges of certifying compilers.

Stainless Tutorial: Verification of Scala Code

Covers the use of Stainless, a verification tool for Scala, to ensure the correctness of Scala code.

Compiler verification: Challenges and Benefits

Explores the challenges and benefits of compiler verification, emphasizing the importance of verifying compilers for critical software.

From Tests to Proof