Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Testing a Claim about Population Proportion01:24

Testing a Claim about Population Proportion

3.5K
A complete procedure for testing a claim about a population proportion is provided here.
There are two methods of testing a claim about a population proportion: (1) Using the sample proportion from the data where a binomial distribution is approximated to the normal distribution and (2) Using the binomial probabilities calculated from the data.
The first method uses normal distribution as an approximation to the binomial distribution. The requirements are as follows: sample size is large...
3.5K
Analysis of Population Pharmacokinetic Data01:12

Analysis of Population Pharmacokinetic Data

425
Analysis of population pharmacokinetic data involves studying the behavior of drugs within diverse populations to understand their pharmacokinetic parameters. Traditional pharmacokinetic methods typically involve collecting samples from a few individuals and estimating these parameters. While these methods are commonly used, they have limitations in capturing the variability in drug response among individuals or heterogeneous populations. Population pharmacokinetics is employed to address these...
425
What are Populations and Communities?00:30

What are Populations and Communities?

35.3K
Overview
35.3K
Microbial Growth Measurement: Direct Methods01:23

Microbial Growth Measurement: Direct Methods

665
Direct methods for measuring microbial populations in a culture are essential tools in microbiology, providing quantitative data for various applications. Among these, microscopic counts, plate counts, and serial dilution are widely used techniques, each with unique principles and applications.Microscopic CountsMicroscopic counting involves the use of a Petroff-Hausser chamber, a specialized microscope slide with a grid and defined depth. By observing a liquid culture under a microscope,...
665
Testing a Claim about Mean: Known Population SD01:11

Testing a Claim about Mean: Known Population SD

2.9K
A complete procedure of testing the hypothesis about a population mean is explained here.
Estimating a population mean requires the samples to be distributed normally. The data should be collected from the randomly selected samples having no sampling bias. The sample size needed to be higher than 30, and most importantly, the population standard deviation should be already known.
In most realistic situations, the population standard deviation is often unknown, but in rare circumstances, when it...
2.9K
What is Population Genetics?01:25

What is Population Genetics?

60.3K
A population is composed of members of the same species that simultaneously live and interact in the same area. When individuals in a population breed, they pass down their genes to their offspring. Many of these genes are polymorphic, meaning that they occur in multiple variants. Such variations of a gene are referred to as alleles. The collective set of all the alleles within a population is known as the gene pool.
60.3K

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

The complexity of verifying population protocols.

Distributed computing·2021
Same journal

Preserving provability over GPU program optimizations with annotation-aware transformations.

Formal methods in system design·2025
Same journal

Golem: a flexible and efficient solver for constrained Horn clauses.

Formal methods in system design·2025
Same journal

Predicate abstraction for hyperliveness verification.

Formal methods in system design·2025
Same journal

Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker.

Formal methods in system design·2024
Same journal

Global guidance for local generalization in model checking.

Formal methods in system design·2024
Same journal

Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version).

Formal methods in system design·2024
See all related articles

Related Experiment Video

Updated: Oct 11, 2025

Heuristic Mining of Hierarchical Genotypes and Accessory Genome Loci in Bacterial Populations
08:03

Heuristic Mining of Hierarchical Genotypes and Accessory Genome Loci in Bacterial Populations

Published on: December 7, 2021

2.5K

Towards efficient verification of population protocols.

Michael Blondin1, Javier Esparza2, Stefan Jaax2

  • 1Département d'informatique, Université de Sherbrooke, 2500 boulevard de l'Université Sherbrooke, Québec, J1K 2R1 Canada.

Formal Methods in System Design
|December 6, 2021
PubMed
Summary
This summary is machine-generated.

This study introduces a new class of protocols for anonymous, identical agents. It presents the first software for automatically verifying population protocol correctness, significantly simplifying complex computations.

Keywords:
Automated verificationPopulation protocolsTermination

More Related Videos

Validating Whole Genome Nanopore Sequencing, using Usutu Virus as an Example
05:45

Validating Whole Genome Nanopore Sequencing, using Usutu Virus as an Example

Published on: March 11, 2020

9.0K
Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly
09:51

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly

Published on: April 25, 2016

7.7K

Related Experiment Videos

Last Updated: Oct 11, 2025

Heuristic Mining of Hierarchical Genotypes and Accessory Genome Loci in Bacterial Populations
08:03

Heuristic Mining of Hierarchical Genotypes and Accessory Genome Loci in Bacterial Populations

Published on: December 7, 2021

2.5K
Validating Whole Genome Nanopore Sequencing, using Usutu Virus as an Example
05:45

Validating Whole Genome Nanopore Sequencing, using Usutu Virus as an Example

Published on: March 11, 2020

9.0K
Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly
09:51

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly

Published on: April 25, 2016

7.7K

Area of Science:

  • Theoretical Computer Science
  • Distributed Computing
  • Formal Verification

Background:

  • Population protocols model computation using anonymous, identical finite-state agents.
  • The well-specification problem, determining if a protocol guarantees consensus from all initial configurations, is known to be highly complex.
  • Previous work established decidability but with TOWER-hard complexity, lacking efficient verification methods.

Purpose of the Study:

  • To introduce a new class of protocols, well-specified strongly-silent protocols ( ), suitable for automatic verification.
  • To demonstrate that protocols possess the same computational power as general well-specified protocols.
  • To develop the first software capable of automatically proving correctness for infinitely many inputs of protocols.

Main Methods:

  • Introduction of the class of well-specified strongly-silent protocols.
  • Mathematical proof of the equivalence in computational power between and general well-specified protocols.
  • Reduction of membership and correctness problems for to solving boolean combinations of linear constraints over .

Main Results:

  • The class is suitable for automatic verification.
  • protocols capture standard protocols found in the literature.
  • The study presents the first software tool for automatically verifying correctness across all possible inputs for protocols.

Conclusions:

  • The proposed protocols offer a practical approach to verifying complex computational systems.
  • Automatic verification of population protocols is now feasible for a significant class of protocols.
  • This work bridges the gap between theoretical models of computation and practical verification tools.