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

Block Diagram Reduction01:22

Block Diagram Reduction

455
The process of deriving the transfer function of a control system often involves reducing its block diagram to a single block. This simplification can be achieved through a series of strategic operations, including relocating branch points and comparators. These operations preserve the overall function of the system while allowing for easier manipulation and combination of blocks.
The first step in this process is the identification and relocation of a branch point. A branch point, where a...
455
The Squeeze Theorem01:30

The Squeeze Theorem

138
Certain mathematical functions exhibit unpredictable or highly variable behavior near specific input values, making direct evaluation of their limits challenging. This complexity may arise from rapid oscillations or irregular patterns that obscure the function’s trend. In such cases, the Squeeze Theorem offers a reliable method for determining limits.According to the Squeeze Theorem, if a function is confined between two other functions near a particular point, and both outer functions...
138
Distribution Reliability and Automation01:25

Distribution Reliability and Automation

440
Distribution reliability in electrical power systems is critical for ensuring an uninterrupted power supply to consumers at minimal cost. According to IEEE Standard Terms, reliability is the probability that a device will function without failure over a specified time period or amount of usage. For electric power distribution, this translates to maintaining continuous power supply and addressing customer concerns over power outages. Several indices, as defined by IEEE Standard 1366-2012, are...
440
Distributed Loads: Problem Solving01:21

Distributed Loads: Problem Solving

1.0K
Beams are structural elements commonly employed in engineering applications requiring different load-carrying capacities. The first step in analyzing a beam under a distributed load is to simplify the problem by dividing the load into smaller regions, which allows one to consider each region separately and calculate the magnitude of the equivalent resultant load acting on each portion of the beam. The magnitude of the equivalent resultant load for each region can be determined by calculating...
1.0K
Multimachine Stability01:25

Multimachine Stability

500
Multimachine stability analysis is crucial for understanding the dynamics and stability of power systems with multiple synchronous machines. The objective is to solve the swing equations for a network of M machines connected to an N-bus power system.
In analyzing the system, the nodal equations represent the relationship between bus voltages, machine voltages, and machine currents. The nodal equation is given by:
500
Model Approaches for Pharmacokinetic Data: Distributed Parameter Models01:06

Model Approaches for Pharmacokinetic Data: Distributed Parameter Models

205
Pharmacokinetic models are mathematical constructs that represent and predict the time course of drug concentrations in the body, providing meaningful pharmacokinetic parameters. These models are categorized into compartment, physiological, and distributed parameter models.
The distributed parameter models are specifically designed to account for variations and differences in some drug classes. This model is particularly useful for assessing regional concentrations of anticancer or...
205

You might also read

Related Articles

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

Sort by
Same author

Empirical software metrics for benchmarking of verification tools.

Formal methods in system design·2020
Same author

Parameterized model checking of rendezvous systems.

Distributed computing·2019
Same author

Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints.

Journal of automated reasoning·2018
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: Dec 29, 2025

Large Scale Energy Efficient Sensor Network Routing Using a Quantum Processor Unit
05:30

Large Scale Energy Efficient Sensor Network Routing Using a Quantum Processor Unit

Published on: September 8, 2023

1.0K

Para : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed

Igor Konnov1, Marijana Lazić1, Helmut Veith1

  • 1Institute of Information Systems E184/4, TU Wien (Vienna University of Technology), Favoritenstraße 9-11, 1040 Vienna, Austria.

Formal Methods in System Design
|February 4, 2020
PubMed
Summary
This summary is machine-generated.

We improved automatic verification for fault-tolerant distributed algorithms (FTDAs). Our new method uses SMT solvers and advanced reductions to efficiently check complex FTDAs, verifying previously unverified algorithms.

Keywords:
Bounded model checkingByzantine faultsCompletenessFault-tolerant distributed algorithmsParameterized verificationPartial orders in distributed systemsReduction

More Related Videos

Plasmid-derived DNA Strand Displacement Gates for Implementing Chemical Reaction Networks
07:50

Plasmid-derived DNA Strand Displacement Gates for Implementing Chemical Reaction Networks

Published on: November 25, 2015

14.8K
Design and Analysis for Fall Detection System Simplification
08:05

Design and Analysis for Fall Detection System Simplification

Published on: April 6, 2020

11.1K

Related Experiment Videos

Last Updated: Dec 29, 2025

Large Scale Energy Efficient Sensor Network Routing Using a Quantum Processor Unit
05:30

Large Scale Energy Efficient Sensor Network Routing Using a Quantum Processor Unit

Published on: September 8, 2023

1.0K
Plasmid-derived DNA Strand Displacement Gates for Implementing Chemical Reaction Networks
07:50

Plasmid-derived DNA Strand Displacement Gates for Implementing Chemical Reaction Networks

Published on: November 25, 2015

14.8K
Design and Analysis for Fall Detection System Simplification
08:05

Design and Analysis for Fall Detection System Simplification

Published on: April 6, 2020

11.1K

Area of Science:

  • Computer Science
  • Distributed Systems
  • Formal Verification

Background:

  • Automatic verification of fault-tolerant distributed algorithms (FTDAs) is complex due to parameterized conditions and system sizes.
  • Existing bounded model checking (BMC) techniques require improvements for verifying state-of-the-art FTDAs.

Purpose of the Study:

  • To enhance the efficiency and completeness of automatic verification for FTDAs.
  • To develop a novel technique for verifying complex FTDAs that were previously intractable.

Main Methods:

  • Encoding bounded executions of counter systems over integer counters in SMT (Satisfiability Modulo Theories).
  • Introducing a new reduction technique exploiting acceleration and FTDA structure to prune the search space.
  • Applying data and counter abstraction followed by bounded model checking.

Main Results:

  • Successfully verified the safety of seven state-of-the-art FTDAs that were previously out of reach.
  • The new SMT-based approach with aggressive pruning significantly improves verification capabilities.

Conclusions:

  • The proposed SMT-based verification technique offers a more powerful and scalable approach for FTDAs.
  • This advancement enables the verification of complex distributed systems, enhancing their reliability.