Wyniki wyszukiwania - BazTech

1

A Framework for the Verification of Parameterized Infinite-state Systems

Alberti F., Ghilardi S., Sharygina N.

Fundamenta Informaticae

|

2017

|

Vol. 150, nr 1

1--24

EN

We present our framework for the verification of parameterized infinite-state systems. The framework has been successfully applied in the verification of heterogeneous systems, ranging from distributed fault-tolerant protocols to programs handling unbounded data-structures. In such application domains, being able to infer quantified invariants is a mandatory requirement for successful results. Our framework differentiates itself from the state-of-the-art solutions targeting the generation of quantified safe inductive invariants: instead of monolitically exploiting a single static analysis technique, it is based on the effective integration of several analysis strategies. The paper targets the description of the engineering strategies adopted for a successful implementation of such an integrated framework, and presents the extensive experimental evaluation demonstrating its effectiveness.

2

Concrete Planning in PlanICS Framework by Combining SMT with GEO and Simulated Annealing

Niewiadomski A., Skaruz J., Switalski P., Penczek W.

Fundamenta Informaticae

|

2016

|

Vol. 147, nr 2/3

289--313

EN

The paper deals with the concrete planning problem – a stage of the web service composition in the PlanICS framework. We present several known and new methods of concrete planning including those based on Satisfiability Modulo Theories (SMT), Genetic Algorithm (GA), as well as methods combining SMT with GA and other nature-inspired algorithms such as Simulated Annealing (SA) and Generalised Extremal Optimization (GEO). The discussion of all the approaches is supported by the complexity analysis, extensive experimental results, and illustrated by a running example.

3

Combining SMT and Simulated Annealing into a Hybrid Planning Method

Skaruz J., Niewiadomski A., Penczek W.

Studia Informatica : systems and information technology

|

2015

|

Vol. 1-2(19)

43--48

EN

We present a new approach to the concrete planning (CP) - a stage of theWeb service composition in the PlanICS framework. A new hybrid algorithm (HSA) based on a combination of Simulated Annealing (SA) with Satisfiability Modulo Theories (SMT) has been designed and implemented. The main idea of our hybrid solution is to use an SMT-based procedure in order to generate an initial individual and then improve it during subsequent iterations of SA. The experimental results show that HSA is superior to the other methods we have applied to the CP problem, including Genetic Algorithm, an SMT-based approach, and our previously developed hybrids.

4

Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem

Morgado A., Marques-Silva J.

Fundamenta Informaticae

|

2010

|

Vol. 102, nr 3/4

363-389

EN

Phylogenetic analysis is a widely used technique, for example in biology and biomedical sciences. The construction of phylogenies can be computationally hard. A commonly used solution for construction of phylogenies is to start from a set of biological species and relations among those species. This work addresses the case where the relations among species are specified as quartet topologies. Moreover, the problem to be solved consists of computing a phylogeny that satisfies the maximum number of quartet topologies. This is referred to as the Maximum Quartet Consistency (MQC) problem, and represents an NP-hard optimization problem. MQC has been solved both heuristically and exactly. Exact solutions forMQC include those based on Constraint Programming, Answer Set Programming, Pseudo-Boolean Optimization (PBO), and SatisfiabilityModulo Theories (SMT). This paper provides a comprehensive overview of the use of PBO and SMT for solving MQC, and builds on recent work in this area. Moreover, the paper provides new insights on how to use SMT for solving optimization problems, by focusing on the concrete case of MQC. The solutions based on PBO and SMT were experimentally compared with other exact solutions. The results show that for instances with small percentage of quartet errors, the models based on SMT can be competitive, whereas for instances with higher number of quartet errors the PBO models are more efficient.