Counterexample guided inductive optimization based on satisfiability modulo theories

Counterexample guided inductive optimization based on satisfiability modulo theories

This paper describes three variants of a counterexample guided inductive optimization (CEGIO) approach based on Satisfiability Modulo Theories (SMT) solvers. In particular, CEGIO relies on iterative executions to constrain a verification procedure, in order to perform inductive generalization, based...

Full description

Bibliographic Details
Main Authors:	Araújo, R, Albuquerque, H, Bessa, d, Cordeiro, L, Chaves Filho, J
Format:	Journal article
Published:	Elsevier 2017

Similar Items

OptCE: A counterexample-guided inductive optimization solver
by: Albuquerque, H, et al.
Published: (2017)

Counterexample guided inductive optimization applied to mobile robots path planning
by: Araújo, R, et al.
Published: (2017)

Counterexample guided inductive synthesis modulo theories
by: Abate, A, et al.
Published: (2018)

Inductive logic programming as satisfiability modulo theories
by: Morel, R
Published: (2023)

A framework for Satisfiability Modulo Theories.
by: Kroening, D, et al.
Published: (2009)

DSValidator: an automated counterexample reproducibility tool for digital systems
by: Chaves, L, et al.
Published: (2018)

SMT-based verification applied to non-convex optimization problems
by: Araujo, R, et al.
Published: (2017)

Counterexample−guided Precondition Inference
by: Seghir, M, et al.
Published: (2013)

Counterexample-guided precondition inference
by: Seghir, M, et al.
Published: (2013)

Verifying Digital Systems with MATLAB
by: Chaves, L, et al.
Published: (2017)

Examples and counterexamples in graph theory /
by: 400749 Capobianco, Michael
Published: (1978)

Formal non-fragile stability verification of digital control systems with uncertainty
by: Bessa, I, et al.
Published: (2016)

Characterizing Boolean satisfiability variants
by: Ferreira Antunes Filho, Ivan Tadeu.
Published: (2020)

Verifying digital systems with MATLAB
by: Chaves, L, et al.
Published: (2017)

Counterexample-Guided Safety Contracts for Autonomous Driving
by: DeCastro, Jonathan, et al.
Published: (2020)

Counterexamples in analysis /
by: 201017 Gelbaum, Bernard R., et al.
Published: (1964)

Counterexamples in probability /
by: 411864 Stoyanov, Jordan M.
Published: (1997)

Counterexamples in topology /
by: Steen, Lynn Arthur, 1941-, et al.
Published: (1978)

VCEGAR: Verilog CounterExample Guided Abstraction Refinement
by: Jain, H, et al.
Published: (2007)

Slopey quantizers are locally optimal for Witsenhausen's counterexample
by: Ajorlou, Amir, et al.
Published: (2017)

Theorems and counterexamples in mathemamatics /
by: 201017 Gelbaum, Bernard R., et al.
Published: (1990)

Modulo-N equalizer
by: 383014 Halim Abd. Aziz
Published: (1977)

Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription
by: Janota, M, et al.
Published: (2010)

Counterexample-guided abstraction refinement for symmetric concurrent programs
by: Donaldson, A, et al.
Published: (2012)

Counterexample Guided Abstraction Refinement via Program Execution
by: Groce, A, et al.
Published: (2004)

Understanding Counterexamples with explain
by: Groce, A, et al.
Published: (2004)

On counterexamples to the Hughes conjecture
by: Havas, G, et al.
Published: (2009)

Satisfiability
by: Hoare, C
Published: (2015)

On graph decompositions modulo k
by: Scott, A
Published: (1997)

A counterexample to metric differentiability
by: Kirchheim, B, et al.
Published: (2003)

Making the most of BMC counterexamples
by: Groce, A, et al.
Published: (2005)

Making the Most of BMC Counterexamples
by: Groce, A, et al.
Published: (2005)

Counterexamples with Loops for Predicate Abstraction
by: Kroening, D, et al.
Published: (2006)

A Counterexample to the Theory that Vision Recovers Three-Dimensional Scenes
by: Marill, Thomas
Published: (2008)

Scale and conformal invariance in field theory: A physical counterexample
by: Riva, V, et al.
Published: (2005)

A Modulo-Based Architecture for Analog-to-Digital Conversion
by: Ordentlich, Or, et al.
Published: (2021)

A Modulo-Based Architecture for Analog-to-Digital Conversion
by: Ordentlich, Or, et al.
Published: (2022)

Satisfied with dissatisfaction?
by: Key, A, et al.
Published: (1999)

On the Littlewood problem modulo a prime
by: Green, B, et al.
Published: (2006)

The distribution of alpha p modulo one
by: Heath-Brown, D, et al.
Published: (2002)