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

Lecture

Property-Based Testing: QuickChick

Description

This lecture by the instructor covers the topic of property-based testing using the tool QuickChick. It delves into the concepts of testing and verification, focusing on software correctness at scale through testing and verification. The lecture discusses the importance of specifications, property-based fuzzing, and a case study on testing noninterference. It also explores dynamic information flow control, correctness in spatial memory safety for C, and the challenges faced in practical property-based testing for Python. The instructor presents the development and application of QuickChick, a property-based testing tool for Coq, highlighting its success stories and the integration of formal verification. The lecture concludes with insights on pushing the limits of property-based testing and the future directions in this field.

This video is available exclusively on Mediaspace for a restricted audience. Please log in to MediaSpace to access it if you have the necessary permissions.

Watch on Mediaspace

Official source

Ontological neighbourhood

Computer engineering

Software development: Software development process

Related concepts (32)

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.

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.

Test automation

In software testing, test automation is the use of software separate from the software being tested to control the execution of tests and the comparison of actual outcomes with predicted outcomes. Test automation can automate some repetitive but necessary tasks in a formalized testing process already in place, or perform additional testing that would be difficult to do manually. Test automation is critical for continuous delivery and continuous testing.

Unit testing

In computer programming, unit testing is a software testing method by which individual units of source code—sets of one or more computer program modules together with associated control data, usage procedures, and operating procedures—are tested to determine whether they are fit for use. It is a standard step in development and implementation approaches such as Agile. Before unit testing, capture and replay testing tools were the norm. In 1997, Kent Beck and Erich Gamma developed and released JUnit, a unit test framework that became popular with Java developers.

Acceptance testing

In engineering and its various subdisciplines, acceptance testing is a test conducted to determine if the requirements of a specification or contract are met. It may involve chemical tests, physical tests, or performance tests. In systems engineering, it may involve black-box testing performed on a system (for example: a piece of software, lots of manufactured mechanical parts, or batches of chemical products) prior to its delivery.

Related lectures (47)

From Tests to Proof

Explores software engineering concepts, emphasizing the significance of tests and clear specifications in ensuring software correctness.

What is Formal Verification?

Introduces formal verification and its advantages over traditional testing methods, discussing automated theorem proving and compiling correctness statements into verification conditions.

Property-Based Testing: Advanced Techniques

Explores advanced software testing techniques, including property-based testing, to ensure code correctness and improve software quality.

Introduction to Formal Verification

Introduces formal verification, emphasizing rigorous proof of system correctness and the use of mathematical models.

Merge Sort: Sorting Algorithm