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

Formal Charges02:42

Formal Charges

40.7K
In some cases, there are seemingly more than one valid Lewis structures for molecules and polyatomic ions. The concept of formal charges can be used to help predict the most appropriate Lewis structure when more than one reasonable structure exists.
40.7K
The Availability Heuristic01:08

The Availability Heuristic

7.1K
A heuristic is a general problem-solving framework (Tversky & Kahneman, 1974). You can think of these as mental shortcuts that are used to solve problems. Different types of heuristics are used in different types of situations, and the impulse to use a heuristic occurs when one of five conditions is met (Pratkanis, 1989):
7.1K
The Representativeness Heuristic02:13

The Representativeness Heuristic

16.8K
The representative heuristic describes a biased way of thinking, in which you unintentionally stereotype someone or something. For example, you may assume that your professors spend their free time reading books and engaging in intellectual conversation, because the idea of them spending their time playing volleyball or visiting an amusement park does not fit in with your stereotypes of professors.
16.8K
The Anchoring-and-Adjustment Heuristic01:25

The Anchoring-and-Adjustment Heuristic

7.8K
In order to make good decisions, we use our knowledge and our reasoning. Often, this knowledge and reasoning is sound and solid. However, sometimes, we are swayed by biases or by others manipulating a situation. For example, let’s say you and three friends wanted to rent a house and had a combined target budget of $1,600. The realtor shows you only very run-down houses for $1,600 and then shows you a very nice house for $2,000. Might you ask each person to pay more in rent to get the...
7.8K
Heuristics01:21

Heuristics

733
Heuristics are problem-solving strategies that use mental shortcuts to simplify decision-making. Unlike algorithms, which must be followed precisely to achieve a correct result, heuristics offer a general problem-solving framework. They save time and energy but can sometimes lead to less rational decisions.
People often rely on heuristics when faced with an overload of information, limited time, low importance of the decision, limited information, or when a heuristic readily comes to mind. For...
733
Lewis Structures and Formal Charges02:19

Lewis Structures and Formal Charges

22.7K
Lewis symbols can be used to indicate the formation of covalent bonds, which are shown in Lewis structures—drawings that describe the bonding in molecules and polyatomic ions. The periodic table can be used to predict the number of valence electrons in an atom and the number of bonds that will be formed to reach an octet. Group 18 elements, such as argon and helium, have filled electron configurations and thus rarely participate in chemical bonding. However, atoms from group 17, such as...
22.7K

You might also read

Related Articles

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

Sort by
Same author

Evidence Generation for a Host-Response Biosignature of Respiratory Disease.

Viruses·2025
Same author

Staged Self-Supervised Learning for Raven Progressive Matrices.

IEEE transactions on neural networks and learning systems·2025
Same author

Modelling of P-wave velocity changes in coal seams with increased depth: a case study.

Scientific reports·2025
Same author

Quantum Annealing in the NISQ Era: Railway Conflict Management.

Entropy (Basel, Switzerland)·2023
Same author

Transcriptomic and Morphological Analysis of Cells Derived from Porcine Buccal Mucosa-Studies on an In Vitro Model.

Animals : an open access journal from MDPI·2020
Same author

Detecting life signatures with RNA sequence similarity measures.

Journal of theoretical biology·2018
Same journal

Computing Optimal Populations for Binary Problems using Logic Minimization.

Evolutionary computation·2026
Same journal

Enhancing Generalization and Scalability for Multi-Objective Optimization with Population Pre-Training.

Evolutionary computation·2026
Same journal

XCS for Sequential Perceptual Aliasing in Multi-Step Decision Making.

Evolutionary computation·2026
Same journal

A dynamic multi-objective evolutionary algorithm using dual-space prediction and surrogate-based sampling.

Evolutionary computation·2026
Same journal

Adapting MOEA/D to CMA-ES for Dealing with Ill-conditioned Multiobjective Problems.

Evolutionary computation·2026
Same journal

Editorial of the Special Issue: Parallel Problem Solving from Nature PPSN 2024 Extended Versions of Best Paper Candidates.

Evolutionary computation·2026
See all related articles

Related Experiment Video

Updated: Feb 10, 2026

Programmed Electrical Stimulation in Mice
07:29

Programmed Electrical Stimulation in Mice

Published on: May 26, 2010

21.3K

Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications.

Iwo Błądek1, Krzysztof Krawiec2, Jerry Swan3

  • 1Institute of Computing Science, Poznan University of Technology, Poznań, 60-965, Poland ibladek@cs.put.poznan.pl.

Evolutionary Computation
|May 23, 2018
PubMed
Summary
This summary is machine-generated.

Counterexample-Based Genetic Programming (CDGP) synthesizes provably correct programs using formal specifications and Satisfiability Modulo Theory (SMT) solvers. This enhanced heuristic reliably generates correct code for arithmetic and string manipulation tasks.

Keywords:
Genetic programmingSMT.counterexamplesformal verification

More Related Videos

Computer-based Multitaper Spectrogram Program for Electroencephalographic Data
04:13

Computer-based Multitaper Spectrogram Program for Electroencephalographic Data

Published on: November 13, 2019

12.8K
Comprehensive Autopsy Program for Individuals with Multiple Sclerosis
09:41

Comprehensive Autopsy Program for Individuals with Multiple Sclerosis

Published on: July 19, 2019

12.1K

Related Experiment Videos

Last Updated: Feb 10, 2026

Programmed Electrical Stimulation in Mice
07:29

Programmed Electrical Stimulation in Mice

Published on: May 26, 2010

21.3K
Computer-based Multitaper Spectrogram Program for Electroencephalographic Data
04:13

Computer-based Multitaper Spectrogram Program for Electroencephalographic Data

Published on: November 13, 2019

12.8K
Comprehensive Autopsy Program for Individuals with Multiple Sclerosis
09:41

Comprehensive Autopsy Program for Individuals with Multiple Sclerosis

Published on: July 19, 2019

12.1K

Area of Science:

  • Computer Science
  • Artificial Intelligence
  • Software Engineering

Background:

  • Conventional genetic programming (GP) relies on input-output examples, offering limited guarantees of program correctness.
  • Formal specification-based program synthesis typically employs exact, non-heuristic algorithms.
  • Counterexample-Based Genetic Programming (CDGP) is an evolutionary heuristic for synthesizing programs from formal specifications.

Purpose of the Study:

  • To extend and improve the Counterexample-Based Genetic Programming (CDGP) heuristic.
  • To enhance the formal verification and fitness calculation mechanisms within CDGP.
  • To evaluate the effectiveness of the improved CDGP on linear integer arithmetic (LIA) and string manipulation (SLIA) benchmarks.

Main Methods:

  • Utilizing a Satisfiability Modulo Theory (SMT) solver for formal verification of candidate programs.
  • Transforming counterexamples generated by the SMT solver into test cases for fitness evaluation.
  • Implementing a fitness threshold parameter to guide the verification process.
  • Introducing a more rigorous method for converting counterexamples into tests.

Main Results:

  • The enhanced CDGP reliably synthesizes provably correct programs across 24 benchmarks in LIA and SLIA domains.
  • CDGP demonstrates effectiveness in generating correct programs compared to state-of-the-art exact synthesis methods.
  • The approach shows a trade-off between synthesis time and resulting program size, favoring smaller programs with longer computation.

Conclusions:

  • The improved CDGP is a robust evolutionary heuristic for synthesizing provably correct programs from formal specifications.
  • CDGP offers a viable alternative to exact methods, particularly when program correctness and size are critical.
  • The study validates CDGP's capability in complex domains like LIA and SLIA, paving the way for further research in evolutionary program synthesis.