Fundamenta Informaticae - Volume 150, issue 1

Authors: Giordano, Laura | Gliozzi, Valentina | Pettorossi, Alberto | Pozzato, Gian Luca

Article Type: Other

DOI: 10.3233/FI-2017-1457

Citation: Fundamenta Informaticae, vol. 150, no. 1, pp. v-vi, 2017

Authors: Alberti, Francesco | Ghilardi, Silvio | Sharygina, Natasha

Article Type: Research Article

Abstract: 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. Show more

Keywords: Infinite-state systems, Software model-checking, Arrays, Quantifiers, Satisfiability Modulo Theories

DOI: 10.3233/FI-2017-1458

Citation: Fundamenta Informaticae, vol. 150, no. 1, pp. 1-24, 2017

Authors: Benedetti, Irene | Bistarelli, Stefano

Article Type: Research Article

Abstract: Formal voting theories are established and can be used to determine if a voting system is fair or not in order to preserve democracy. There are a lot of voting systems described in the literature, with several properties, useful in many contexts. The Argumentation Framework is based on the exchange and the evaluation of interacting arguments which may represent information of various kinds. We show that Argumentation Frameworks can be interpreted within a voting theory and considered as voting methods. Using a mapping that associates an argument to a candidate and attacks to votes, we define a bidirectional mapping between …the two theories and investigate how fairness criteria defined for voting systems can be re-interpreted within Argumentation Framework. We also show how voting ballots can be seen as suitable semantics for Argumentation Frameworks. Show more

Keywords: Argumentation Framework, Voting System, Arrow Fairness Criteria, Balloting Systems, Dichotomic Preferences

DOI: 10.3233/FI-2017-1459

Citation: Fundamenta Informaticae, vol. 150, no. 1, pp. 25-48, 2017

Authors: Cantone, Domenico | Longo, Cristiano | Nicolosi-Asmundo, Marianna

Article Type: Research Article

Abstract: In the last decades, several fragments of set theory have been studied in the context of Computable Set Theory . In general, the semantics of set-theoretic languages differs from the canonical first-order semantics in that the interpretation domain of set-theoretic terms is fixed to a given universe of sets. Because of this, theoretical results and various machinery developed in the context of first-order logic could be not easily applicable in the set-theoretic realm. Recently, the decidability of quantified fragments of set theory which allow one to explicitly handle ordered pairs has been studied, in view of applications in the field …of knowledge representation. Among other results, a NEXP TIME decision procedure for satisfiability of formulae in one of these fragments, ∀ 0 π , has been devised. In this paper we exploit the main features of such a decision procedure to reduce the satisfiability problem for the fragment ∀ 0 π to the problem of Herbrand satisfiability for a first-order language extending it. In addition, it turns out that such a reduction maps formulae of the Disjunctive Datalog subset of ∀ 0 π into Disjunctive Datalog formulae. Show more

DOI: 10.3233/FI-2017-1460

Citation: Fundamenta Informaticae, vol. 150, no. 1, pp. 49-71, 2017

Authors: De Angelis, Emanuele | Fioravanti, Fabio | Pettorossi, Alberto | Proietti, Maurizio

Article Type: Research Article

Abstract: The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program T , and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program …with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog . In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull . Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature. Show more

Keywords: Constraint Handling Rules, Constraint logic programming, Program transformation, Program verification

DOI: 10.3233/FI-2017-1461

Citation: Fundamenta Informaticae, vol. 150, no. 1, pp. 73-117, 2017

Authors: Ferrari, Mauro | Fiorentini, Camillo | Fiorino, Guido

Article Type: Research Article

Abstract: JTabWb is a Java framework for developing provers based on sequent or tableau calculi. It provides a generic engine which searches for proof of a given goal driven by a user-defined prover. The user is required to define the components of a prover by implementing suitable Java interfaces. In this paper we describe the structure of the framework and the role of its components through a running example. To show the generality of the framework we review some of the provers implemented in JTabWb. Finally, to corroborate the fact that the framework can be used to generate efficient provers, we …compare the performances of one of the implemented provers with the state-of-the-art provers for Intuitionistic Propositional Logic. Show more

Keywords: Theorem provers, Java frameworks

DOI: 10.3233/FI-2017-1462

Citation: Fundamenta Informaticae, vol. 150, no. 1, pp. 119-142, 2017