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

Protein Folding Quality Check in the RER01:29

Protein Folding Quality Check in the RER

5.1K
ER is the primary site for the maturation and folding of soluble and transmembrane secretory proteins. The calnexin cycle is a specific chaperone system that folds and assesses the confirmation of N-glycosylated proteins before they can exit the ER lumen. The primary players of this quality check pipeline are the lectins, ER-resident chaperones, and a glucosyl transferase enzyme. In case the calnexin system in the lumen fails to salvage a misfolded protein, it is transported to the cytoplasm...
5.1K
Improving Translational Accuracy02:07

Improving Translational Accuracy

14.1K
Base complementarity between the three base pairs of mRNA codon and the tRNA anticodon is not a failsafe mechanism. Inaccuracies can range from a single mismatch to no correct base pairing at all. The free energy difference between the correct and nearly correct base pairs can be as small as 3 kcal/ mol. With complementarity being the only proofreading step, the estimated error frequency would be one wrong amino acid in every 100 amino acids incorporated. However, error frequencies observed in...
14.1K
Improving Translational Accuracy02:07

Improving Translational Accuracy

3.6K
3.6K
Photoluminescence: Applications01:14

Photoluminescence: Applications

1.0K
Photoluminescence offers a wide range of applications due to its inherent sensitivity and selectivity. This technique allows for both direct and indirect analyses of the analyte. Direct quantitative analysis is possible when the analyte exhibits a favorable quantum yield for fluorescence or phosphorescence. However, an indirect analysis may be feasible if the analyte is not fluorescent or phosphorescent, or if the quantum yield is unfavorable. Indirect methods include reacting the analyte with...
1.0K
Radiation: Applications01:17

Radiation: Applications

1.7K
The average temperature of Earth is the subject of much current discussion. Earth is in radiative contact with both the Sun and dark space; it receives almost all its energy from the radiation of the Sun and reflects some of it into outer space. Dark space is very cold, about 3 K, so Earth radiates energy into it. For instance, heat transfer occurs from soil and grasses, the rate of which can be so rapid that frost can occur on clear summer evenings, even in warm latitudes.
The average...
1.7K
Applications of Stress01:04

Applications of Stress

658
Consider a structure made of a boom and a rod designed to support a load. These two components are connected by a pin and stabilized by brackets and pins. The boom and the rod are detached from their supports to assess the different stresses imposed on this structure, and a free-body diagram is drawn. Then, all the forces applied, including the load acting on the structure, are identified. The reaction forces exerted on both the boom and the rod are computed using the equilibrium equations.
The...
658

You might also read

Related Articles

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

Sort by
Same author

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

Formal methods in system design·2025
Same author

Trident: Three-dimensional ray tracing for modeling high intensity focused ultrasound ablation.

The Journal of the Acoustical Society of America·2025
Same author

Mathematical multi-compartment modeling of chronic lymphocytic leukemia cell kinetics under ibrutinib.

iScience·2024
Same author

Merging Modular Molecular Design with High Throughput Screening of Cell Adhesion on Antimicrobial Supramolecular Biomaterials.

Macromolecular rapid communications·2024
Same author

Tens of images can suffice to train neural networks for malignant leukocyte detection.

Scientific reports·2021
Same author

Reconn: a cytoscape plug-in for exploring and visualizing reactome.

Journal of bioinformatics and computational biology·2013
Same journal

A technology transfer journey to a model-driven access control system.

International journal on software tools for technology transfer : STTT·2023
Same journal

Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020.

International journal on software tools for technology transfer : STTT·2022
Same journal

PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives.

International journal on software tools for technology transfer : STTT·2019
Same journal

Guided search for hybrid systems based on coarse-grained space abstractions.

International journal on software tools for technology transfer : STTT·2016
Same journal

Witnessing the elimination of magic wands.

International journal on software tools for technology transfer : STTT·2016
See all related articles

Related Experiment Video

Updated: Jan 26, 2026

Application of a Coupling Agent to Improve the Dielectric Properties of Polymer-Based Nanocomposites
06:34

Application of a Coupling Agent to Improve the Dielectric Properties of Polymer-Based Nanocomposites

Published on: September 19, 2020

6.3K

Model checking: recent improvements and applications.

Dragan Bošnački1, Anton Wijs1

  • 1Eindhoven University of Technology, Eindhoven, The Netherlands.

International Journal on Software Tools for Technology Transfer : STTT
|April 9, 2019
PubMed
Summary
This summary is machine-generated.

Model checking is an automatic formal verification technique for concurrent systems. This research explores advancements in model checking, focusing on improving scalability and expanding its use for planning and quantitative analysis.

Keywords:
Model checkingPartial-order reductionPlanningProbabilistic model checkingStrategy synthesis

More Related Videos

Improved Rodent Model of Myocardial Ischemia and Reperfusion Injury
07:23

Improved Rodent Model of Myocardial Ischemia and Reperfusion Injury

Published on: March 7, 2022

7.2K
Improving 2D and 3D Skin In Vitro Models Using Macromolecular Crowding
09:14

Improving 2D and 3D Skin In Vitro Models Using Macromolecular Crowding

Published on: August 22, 2016

13.0K

Related Experiment Videos

Last Updated: Jan 26, 2026

Application of a Coupling Agent to Improve the Dielectric Properties of Polymer-Based Nanocomposites
06:34

Application of a Coupling Agent to Improve the Dielectric Properties of Polymer-Based Nanocomposites

Published on: September 19, 2020

6.3K
Improved Rodent Model of Myocardial Ischemia and Reperfusion Injury
07:23

Improved Rodent Model of Myocardial Ischemia and Reperfusion Injury

Published on: March 7, 2022

7.2K
Improving 2D and 3D Skin In Vitro Models Using Macromolecular Crowding
09:14

Improving 2D and 3D Skin In Vitro Models Using Macromolecular Crowding

Published on: August 22, 2016

13.0K

Area of Science:

  • Computer Science
  • Software Engineering

Background:

  • Model checking is an automatic formal verification technique for concurrent systems.
  • It verifies functional properties, detects errors with counter-examples, but suffers from scalability limitations.

Purpose of the Study:

  • To address the scalability challenges in model checking.
  • To explore the application of model checking for planning and quantitative analysis.

Main Methods:

  • Review of selected papers from the 23rd International SPIN Symposium on Model Checking Software (SPIN 2016).
  • Discussion of contributions focused on reducing computational effort and expanding model checking's scope.

Main Results:

  • Several contributions address model checking's scalability issues.
  • New approaches enable model checking for planning and quantitative property verification.

Conclusions:

  • Research presented enhances the efficiency and applicability of model checking.
  • These advancements are crucial for verifying complex concurrent systems.