Lower-Bound Synthesis Using Loop Specialization and Max-SMT
| Autor: | Samir Genaim, Elvira Albert, Albert Rubio, Enrique Martin-Martin, Alicia Merayo |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Computer science
020207 software engineering 0102 computer and information sciences 02 engineering and technology Function (mathematics) Solver 01 natural sciences Upper and lower bounds Image (mathematics) Loop (topology) 010201 computation theory & mathematics Encoding (memory) Specialization (functional) 0202 electrical engineering electronic engineering information engineering Algorithm Integer (computer science) |
| Zdroj: | Computer Aided Verification ISBN: 9783030816872 CAV (2) |
| DOI: | 10.1007/978-3-030-81688-9_40 |
| Popis: | This paper presents a new framework to synthesize lower-bounds on the worst-case cost for non-deterministic integer loops. As in previous approaches, the analysis searches for a metering function that under-approximates the number of loop iterations. The key novelty of our framework is the specialization of loops, which is achieved by restricting their enabled transitions to a subset of the inputs combined with the narrowing of their transition scopes. Specialization allows us to find metering functions for complex loops that could not be handled before or be more precise than previous approaches. Technically, it is performed (1) by using quasi-invariants while searching for the metering function, (2) by strengthening the loop guards, and (3) by narrowing the space of non-deterministic choices. We also propose a Max-SMT encoding that takes advantage of the use of soft constraints to force the solver look for more accurate solutions. We show our accuracy gains on benchmarks extracted from the 2020 Termination and Complexity Competition by comparing our results to those obtained by the "Image missing" system. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|