Evolving SMT Strategies
| Autor: | Frédéric Saubion, Nicolas Galvez Ramirez, Eric Monfroy, Youssef Hamadi |
|---|---|
| Přispěvatelé: | Laboratoire d'Etudes et de Recherche en Informatique d'Angers (LERIA), Université d'Angers (UA), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Laboratoire d'Informatique de Nantes Atlantique (LINA), Centre National de la Recherche Scientifique (CNRS)-Mines Nantes (Mines Nantes)-Université de Nantes (UN) |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Theoretical computer science
Programming language Semantics (computer science) Computer science Modulo Evolutionary algorithm 020207 software engineering 02 engineering and technology 010501 environmental sciences computer.software_genre 01 natural sciences Evolutionary computation Satisfiability modulo theories 0202 electrical engineering electronic engineering information engineering [INFO]Computer Science [cs] Heuristics computer 0105 earth and related environmental sciences |
| Zdroj: | 28th IEEE International Conference on Tools with Artificial Intelligence (ICTAI) 28th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2016, San Jose, United States ICTAI |
| Popis: | StratEVO is an evolutionary algorithm that aims at generating strategies for the SMT solver Z3. Solving SAT modulo theories instance requires to define complex combinations of solvers, heuristics and proof checking tools that require expert knowledge. Our purpose is thus to show that an automated strategy generation process can be efficient and allows end-users to avoid difficult configuration tasks when using such solvers. StratEVO is evaluated on benchmarks from the 2014 and 2015 SMT competitions. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|