Peleska, JanFopoussi Nono, Serge AchilleSerge AchilleFopoussi Nono2020-03-102020-03-102010-06-28https://media.suub.uni-bremen.de/handle/elib/2829In this dissertation we present an incremental approach to solve the Satisfiability (SAT) Problem for the automated test case generation of hybrid discrete and continuous embedded systems using background theory solvers of the linear arithmetic (LA) and fixed-size bit-vectors (BV) for quantifier-free first-order formulae. Both of these theory solvers extend the Davis-Putnam-Logemann-Loveland decision procedure (DPLL), which was initially designed to solve the satisfiability problem in the propositional logic, to the first-order logic. Furthermore the both theory solvers can be integrated in a lazy SMT-Theorem Prover - also known as Satisfiability Modulo Theory - as a decision procedure for the conjunction of literals in their specified theories and implement theory-driven deduction, learning and backjumping techniques to enhance the efficiency of the SMT-Theorem Prover.deBitte wählen Sie eine Lizenz aus: (Unsere Empfehlung: CC-BY)Test AutomationSatisfiability Modulo TheoriesDPLLSATInterval AnalysisFourier Motzkin eliminationbit-vectorslinear arithmeticHYBIS constraint solverHYLIS constraint solverthree-valued logicGalois Connections80Dissertationurn:nbn:de:gbv:46-diss000119525