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

Language and Cognition01:27

Language and Cognition

681
Language serves as a bridge between ideas and communication, influencing how individuals perceive and interact with the world. Psychologists have long debated whether language shapes thought or vice versa. This discussion gained grip with Edward Sapir and Benjamin Lee Whorf in the 1940s, who proposed that language determines thought, a concept known as linguistic determinism. They suggested that the vocabulary and structure of a language influence how its speakers think and perceive reality.
681
Language Development01:22

Language Development

801
Children master language quickly and with relative ease, supported by both biological predisposition and reinforcement. B. F. Skinner (1957) proposed that language is learned through reinforcement, while Noam Chomsky (1965) argued that language acquisition mechanisms are biologically determined.
The critical period for language acquisition suggests that the ability to acquire language is at its peak early in life. As people age, this proficiency decreases. Language development begins very...
801
Synthetic Biology02:55

Synthetic Biology

5.5K
Synthetic biology is an interdisciplinary science that involves using principles from disciplines such as engineering, molecular biology, cell biology, and systems biology. It involves remodeling existing organisms from nature or constructing completely new synthetic organisms for applications such as protein or enzyme production, bioremediation, value-added macromolecule production, and the addition of desirable traits to crops, to name a few.
Golden rice
Golden rice is a genetically modified...
5.5K
Improving Translational Accuracy02:07

Improving Translational Accuracy

3.5K
3.5K
Improving Translational Accuracy02:07

Improving Translational Accuracy

14.0K
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.0K
Language01:16

Language

855
Language is a unique communication system that uses words and systematic rules to organize and transmit information. Unlike other forms of communication, which may involve postures, movements, odors, or vocalizations, language relies on symbols and grammar. This makes human communication distinct from that of other species, who also communicate but do not use language in the same way humans do.
Corballis and Suddendorf (2007) and Tomasello and Rakoczy (2003) highlight the role of language in...
855

You might also read

Related Articles

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

Sort by
Same author

Breakthrough mucormycosis after hematopoietic stem cell transplantation: a retrospective multiyear cohort study in Eastern China.

Annals of clinical microbiology and antimicrobials·2026
Same author

Fatty Acid-Binding Protein 4 and Major Adverse Cardiovascular Events: A Dose-Response Meta-Analysis of Prospective Cohort Studies.

European journal of preventive cardiology·2026
Same author

<i>Hex</i>-MASP for Mapping the Whole-tissue Spatial Proteome and the Intra-brain Distribution of Monoclonal Antibodies.

bioRxiv : the preprint server for biology·2026
Same author

Tetrandrine, a Major Alkaloid From <i>Stephaniae Tetrandrae Radix</i>, Ameliorates Non-Alcoholic Fatty Liver Disease in Zebrafish via the PI3K/AKT/STAT3 Pathway.

Food science & nutrition·2026
Same author

Social jet lag and visual acuity decline in junior high students: a retrospective cohort study.

Scientific reports·2026
Same author

Impact of intraoperative nonsteroidal anti-inflammatory drugs on acute kidney injury after major noncardiac surgery: a propensity score-matched analysis.

Renal failure·2026

Related Experiment Video

Updated: Jan 7, 2026

Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems
05:47

Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems

Published on: June 13, 2025

1.2K

KerSpecGen: Co-piloting formal Kernel specification synthesis with refined knowledge graphs and large language

Zi Wang1, Xiaoyu Zhu2, Hongqiang Wang2

  • 1School of Cyber Science and Technology, Beihang University, Beijing, China.

Plos One
|December 31, 2025
PubMed
Summary

This study introduces KerSpecGen, a Large Language Model (LLM) framework that automatically synthesizes formal kernel specifications for complex microkernels. KerSpecGen significantly reduces the manual effort required for formal verification, improving efficiency.

More Related Videos

Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness
03:14

Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness

Published on: December 6, 2024

983
Constructing and Visualizing Models using Mime-based Machine-learning Framework
06:19

Constructing and Visualizing Models using Mime-based Machine-learning Framework

Published on: July 22, 2025

2.2K

Related Experiment Videos

Last Updated: Jan 7, 2026

Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems
05:47

Evidence-based Knowledge Synthesis and Hypothesis Validation: Navigating Biomedical Knowledge Bases via Explainable AI and Agentic Systems

Published on: June 13, 2025

1.2K
Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness
03:14

Augmenting Large Language Models via Vector Embeddings to Improve Domain-Specific Responsiveness

Published on: December 6, 2024

983
Constructing and Visualizing Models using Mime-based Machine-learning Framework
06:19

Constructing and Visualizing Models using Mime-based Machine-learning Framework

Published on: July 22, 2025

2.2K

Area of Science:

  • Computer Science
  • Software Engineering
  • Formal Methods

Background:

  • Formal verification is crucial for software correctness but challenging for complex microkernels like seL4 due to labor-intensive specification writing.
  • Existing methods are expertise-dependent and limited, hindering the practical application of formal methods in microkernel development.

Purpose of the Study:

  • To propose KerSpecGen, a novel framework utilizing Large Language Models (LLMs) to automate the synthesis of formal kernel specifications.
  • To address the limitations of manual specification writing for complex microkernels, thereby enhancing the practicality of formal verification.

Main Methods:

  • Developed KerSpecGen, an LLM-based framework integrating knowledge graphs to connect requirement descriptions with specification properties.
  • Constructed a refined knowledge graph with deduplication, property judgment, and source annotation for accuracy.
  • Created a custom dataset for fine-tuning a model to convert specification properties into code, and designed LLM-oriented templates for generating complete specifications.

Main Results:

  • KerSpecGen demonstrated superior performance over the Few-shot method, achieving an average of 7.06 percentage points higher in BLEU-4 on the KerSpecProperty benchmark.
  • The framework produced better specification quality in 23 out of 30 seL4 function modules when using the Llama-3.1-405B model.
  • Generated specifications are high-quality reference artifacts, substantially reducing the burden of manual specification writing.

Conclusions:

  • KerSpecGen represents a significant advancement in automating formal specification generation for complex microkernels.
  • The framework effectively bridges requirement descriptions and formal properties using LLMs and knowledge graphs.
  • While minor adjustments may be needed for direct execution, KerSpecGen substantially lowers the barrier to entry for formal verification in microkernel systems.