Search research articles

ABOUT JoVE

Overview Leadership Blog JoVE Help Center

AUTHORS

Publishing Process Editorial Board Scope & Policies Peer Review FAQ Submit

LIBRARIANS

Testimonials Subscriptions Access Resources Library Advisory Board FAQ

RESEARCH

JoVE Journal Methods Collections JoVE Encyclopedia of Experiments Archive

EDUCATION

JoVE Core JoVE Business JoVE Science Education JoVE Lab Manual Faculty Resource Center Faculty Site

Terms & Conditions of Use

Related Concept Videos

Nonsense-mediated mRNA Decay

Nonsense-mediated mRNA Decay

The Upf proteins that carry out nonsense-mediated decay (NMD) are found in all eukaryotic organisms, including humans. Each protein has an individual role, but they need to work in collaboration. Upf1 is an ATP-dependent RNA helicase that unwinds the RNA helix. Because Upf1 can unwind any RNA, Upf2 and Upf3 are required to help Upf1 discriminate between nonsense and normal mRNAs.
Usually, Upf3 binds to an Exon Junction Complex (EJC) at mRNA splice sites. If a ribosome fully translates the mRNA,...

Transcription Attenuation in Prokaryotes

Transcription Attenuation in Prokaryotes

Transcriptional attenuation occurs when RNA transcription is prematurely terminated due to the formation of a terminator mRNA hairpin structure. Bacteria use these hairpins to regulate the transcription process and control the synthesis of several amino acids including histidine, lysine, threonine, and phenylalanine. Transcription attenuation takes place in the non-coding regions of mRNA.
There are several different mechanisms used to attenuate transcription. In ribosome mediated...

Survival Tree

Survival Tree

Survival trees are a non-parametric method used in survival analysis to model the relationship between a set of covariates and the time until an event of interest occurs, often referred to as the "time-to-event" or "survival time." This method is particularly useful when dealing with censored data, where the event has not occurred for some individuals by the end of the study period, or when the exact time of the event is unknown.
Building a Survival Tree
Constructing a...

You might also read

Related Articles

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

Sort by

Same author

Scenario-Based Verification of Uncertain MDPs.

Tools and algorithms for the construction and analysis of systems : 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, ...·2020

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

Search research articles

Related Experiment Video

Updated: Jul 9, 2025

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

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

Published on: April 25, 2016

The probabilistic termination tool amber.

Marcel Moosbrugger¹, Ezio Bartocci¹, Joost-Pieter Katoen²

¹TU Wien, Vienna, Austria.

Formal Methods in System Design

|December 4, 2023

Summary

This summary is machine-generated.

Amber is a new automated tool that proves or disproves the termination of probabilistic while-programs. It uses martingale theory and bounding functions, outperforming current state-of-the-art tools in experiments.

Keywords:

Almost sure termination Asymptotic bounds Martingales Probabilistic programs Recurrence equations

More Related Videos

Exploring Caspase Mutations and Post-Translational Modification by Molecular Modeling Approaches

Exploring Caspase Mutations and Post-Translational Modification by Molecular Modeling Approaches

Published on: October 13, 2022

Author Spotlight: In Silico Creation and Impact of Carbonylated Amino Acids on Protein Structure and Function

Author Spotlight: In Silico Creation and Impact of Carbonylated Amino Acids on Protein Structure and Function

Published on: April 26, 2024

Related Experiment Videos

Last Updated: Jul 9, 2025

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

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

Published on: April 25, 2016

Exploring Caspase Mutations and Post-Translational Modification by Molecular Modeling Approaches

Exploring Caspase Mutations and Post-Translational Modification by Molecular Modeling Approaches

Published on: October 13, 2022

Author Spotlight: In Silico Creation and Impact of Carbonylated Amino Acids on Protein Structure and Function

Author Spotlight: In Silico Creation and Impact of Carbonylated Amino Acids on Protein Structure and Function

Published on: April 26, 2024

Area of Science:

Computer Science
Automated Reasoning
Probabilistic Programming

Background:

Automated termination analysis is crucial for program correctness.
Probabilistic programs introduce complexities in termination verification.
Existing tools struggle with programs involving polynomial arithmetic.

Purpose of the Study:

To introduce the Amber tool for automated termination analysis of probabilistic while-programs.
To address the challenge of proving/disproving termination for programs with polynomial arithmetic.
To provide a more effective solution compared to existing state-of-the-art tools.

Main Methods:

Amber combines martingale theory with asymptotic bounding functions.
It implements relaxed probabilistic termination proof rules.
The tool handles symbolic constants and common probability distributions.

Main Results:

Amber successfully proves and refutes termination for a class of probabilistic while-programs.
Experimental comparisons demonstrate Amber's superior performance.
The tool achieves automated verification in a fully automated manner.

Conclusions:

Amber offers an effective automated solution for probabilistic program termination analysis.
The tool's approach advances the field of automated reasoning for probabilistic systems.
Amber provides practical advantages over existing state-of-the-art termination analysis tools.