Cimatti A.,FBK irst |
Griggio A.,University of Trento |
Sebastiani R.,University of Trento
ACM Transactions on Computational Logic | Year: 2010
The problem of computing Craig interpolants has recently received a lot of interest. In this article, we address the problem of efficient generation of interpolants for some important fragments of first-order logic, which are amenable for effective decision procedures, called satisfiability modulo theory (SMT) solvers. We make the following contributions. First, we provide interpolation procedures for several basic theories of interest: the theories of linear arithmetic over the rationals, difference logic over rationals and integers, and UTVPI over rationals and integers. Second, we define a novel approach to interpolate combinations of theories that applies to the delayed theory combination approach. Efficiency is ensured by the fact that the proposed interpolation algorithms extend state-of-the-art algorithms for satisfiability modulo theories. Our experimental evaluation shows that the MathSAT SMT solver can produce interpolants with minor overhead in search, and much more efficiently than other competitor solvers. © 2010 ACM.
Dragoni M.,FBK irst
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2015
Ontology mapping is a task aiming to align semantic resources in order to foster the re-use of information and to enable the knowledge and data expressed in the matched ontologies to interoperate. When ontology mapping algorithms are applied in practice, a manual refinement is furtherly necessary for validating the correctness of the resulted resource, especially, as it happens in real-world cases, when a gold standard cannot be exploited for assessing the generated mappings. In this paper, we present a suggestion-based mapping system, integrated as a component of a knowledge management platform, implementing an information retrieval-based (IR-based) approach for generating and validating, by experts, mappings between ontologies. The proposed platform has been evaluated quantitatively (i.e. effectiveness of suggestions, reduction of the user effort, etc.) and qualitatively (i.e. usability) on two use cases: Organic. Lingua and PRESTO, respectively an EU-funded and regional-funded projects. The results demonstrated the effectiveness and usability of the proposed platform in a real-world environment. © Springer International Publishing Switzerland 2015.
Schuppan V.,FBK irst
Science of Computer Programming | Year: 2012
Unsatisfiable cores, i.e., parts of an unsatisfiable formula that are themselves unsatisfiable, have important uses in debugging specifications, speeding up search in model checking or SMT, and generating certificates of unsatisfiability. While unsatisfiable cores have been well investigated for Boolean SAT and constraint programming, the notion of unsatisfiable cores for temporal logics such as LTL has not received much attention. In this paper we investigate notions of unsatisfiable cores for LTL that arise from the syntax tree of an LTL formula, from converting it into a conjunctive normal form, and from proofs of its unsatisfiability. The resulting notions are more fine-grained than existing ones. We illustrate the benefits of the more fine-grained notions on examples from the literature. We extend some of the notions to realizability and we discuss the relationship of unsatisfiable and unrealizable cores with the notion of vacuity. © 2010 Elsevier B.V. All rights reserved.
Ghilardi S.,University of Milan |
Ranise S.,FBK irst
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2010
We describe mcmt, a fully declarative and deductive symbolic model checker for safety properties of infinite state systems whose state variables are arrays. Theories specify the properties of the indexes and the elements of the arrays. Sets of states and transitions of a system are described by quantified first-order formulae. The core of the system is a backward reachability procedure which symbolically computes pre-images of the set of unsafe states and checks for safety and fix-points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics for quantifier instantiation, specifically tailored to model checking, are at the very heart of the system. mcmt has been successfully applied to the verification of imperative programs, parametrised, timed, and distributed systems. © 2010 Springer-Verlag.
Ranise S.,FBK irst
Formal Methods in System Design | Year: 2013
We describe a symbolic procedure for solving the reachability problem of transition systems that use formulae of Effectively Propositional Logic to represent sets of backward reachable states. We discuss the key ideas for the mechanization of the procedure where fix-point checks are reduced to SMT problems. We also show the termination of the procedure on a sub-class of transition systems. Then, we discuss how reachability problems for this sub-class can be used to encode analysis problems of administrative policies in the Role-Based Access Control (RBAC) model that is one of the most widely adopted access control paradigms. An implementation of a refinement of the backward reachability procedure, called asasp, shows better flexibility and scalability than a state-of-the-art tool on a significant set of security problems. © 2012 Springer Science+Business Media, LLC.