ART - TORVERGATA OAhttps://art.torvergata.itIl sistema di repository digitale IRIS acquisisce, archivia, indicizza, conserva e rende accessibili prodotti digitali della ricerca.Mon, 12 Apr 2021 06:19:54 GMT2021-04-12T06:19:54Z10801Improving reachability analysis of infinite state systems by specializationhttp://hdl.handle.net/2108/76469Titolo: Improving reachability analysis of infinite state systems by specialization
Abstract: We consider infinite state reactive systems specified by using linear constraints over the integers, and we address the problem of verifying safety properties of these systems by applying reachability analysis techniques. We propose a method based on program specialization, which improves the effectiveness of the backward and forward reachability analyses. For backward reachability our method consists in: (i) specializing the reactive system with respect to the initial states, and then (ii) applying to the specialized system the reachability analysis that works backwards from the unsafe states. For reasons of efficiency, during specialization we make use of a relaxation from integers to reals. In particular, we test the satisfiability or entailment of constraints over the real numbers, while preserving the reachability properties of the reactive systems when constraints are interpreted over the integers. For forward reachability our method works as for backward reachability, except that the role of the initial states and the unsafe states are interchanged. We have implemented our method using the MAP transformation system and the ALV verification system. Through various experiments performed on several infinite state systems, we have shown that our specialization-based verification technique considerably increases the number of successful verifications without a significant degradation of the time performance.
Sun, 01 Jan 2012 00:00:00 GMThttp://hdl.handle.net/2108/764692012-01-01T00:00:00ZConstraint-based correctness proofs for logic program transformationshttp://hdl.handle.net/2108/75590Titolo: Constraint-based correctness proofs for logic program transformations
Abstract: Many approaches proposed in the literature for proving the correctness of unfold/fold transformations of logic programs make use of measures associated with program clauses. When from a program P 1 we derive a program P 2 by applying a sequence of transformations, suitable conditions on the measures of the clauses in P 2 guarantee that the transformation of P 1 into P 2 is correct, that is, P 1 and P 2 have the same least Herbrand model. In the approaches proposed so far, clause measures are fixed in advance, independently of the transformations to be proved correct. In this paper we propose a method for the automatic generation of clause measures which, instead, takes into account the particular program transformation at hand. During the application of a sequence of transformations we construct a system of linear equalities and inequalities over nonnegative integers whose unknowns are the clause measures to be found, and the correctness of the transformation is guaranteed by the satisfiability of that system. Through some examples we show that our method is more powerful and practical than other methods proposed in the literature. In particular, we are able to establish in a fully automatic way the correctness of program transformations which, by using other methods, are proved correct at the expense of fixing in advance sophisticated clause measures.
Sun, 01 Jan 2012 00:00:00 GMThttp://hdl.handle.net/2108/755902012-01-01T00:00:00ZGeneralization strategies for the verification of infinite state systemshttp://hdl.handle.net/2108/76107Titolo: Generalization strategies for the verification of infinite state systems
Abstract: We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools.
Tue, 01 Jan 2013 00:00:00 GMThttp://hdl.handle.net/2108/761072013-01-01T00:00:00ZSoftware model checking by program specializationhttp://hdl.handle.net/2108/75594Titolo: Software model checking by program specialization
Sun, 01 Jan 2012 00:00:00 GMThttp://hdl.handle.net/2108/755942012-01-01T00:00:00ZImproving reachability analysis of infinite state systems by specializationhttp://hdl.handle.net/2108/70207Titolo: Improving reachability analysis of infinite state systems by specialization
Sat, 01 Jan 2011 00:00:00 GMThttp://hdl.handle.net/2108/702072011-01-01T00:00:00ZProgram transformation for development, verification, and synthesis of programshttp://hdl.handle.net/2108/70208Titolo: Program transformation for development, verification, and synthesis of programs
Sat, 01 Jan 2011 00:00:00 GMThttp://hdl.handle.net/2108/702082011-01-01T00:00:00ZSynthesizing concurrent programs using answer set programminghttp://hdl.handle.net/2108/70150Titolo: Synthesizing concurrent programs using answer set programming
Sat, 01 Jan 2011 00:00:00 GMThttp://hdl.handle.net/2108/701502011-01-01T00:00:00ZControlling polyvariance for specialization-based verificationhttp://hdl.handle.net/2108/76487Titolo: Controlling polyvariance for specialization-based verification
Abstract: Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise
Tue, 01 Jan 2013 00:00:00 GMThttp://hdl.handle.net/2108/764872013-01-01T00:00:00ZSpecialization with Constrained Generalization for Software Model Checkinghttp://hdl.handle.net/2108/76507.1Titolo: Specialization with Constrained Generalization for Software Model Checking
Tue, 01 Jan 2013 00:00:00 GMThttp://hdl.handle.net/2108/76507.12013-01-01T00:00:00ZVerification of imperative programs through transformation of constraint logic programshttp://hdl.handle.net/2108/76527Titolo: Verification of imperative programs through transformation of constraint logic programs
Tue, 01 Jan 2013 00:00:00 GMThttp://hdl.handle.net/2108/765272013-01-01T00:00:00Z