@proceedings {CominiGL01, title = {How to Transform an Analyzer into a Verifier}, journal = {Logic for Programming and Automated Reasoning. Proceedings of the 8th International Conference (LPAR{\textquoteright}01)}, volume = {2250}, year = {2001}, pages = {595{\textendash}609}, publisher = {Springer-Verlag}, address = {Berlin}, abstract = {In this paper we push forward the idea of applying the abstract interpretation concepts to the problem of verification of programs. We consider the theory of abstract verification as proposed in [CominiGLV99entcs,CominiGLV99] and we show how it is possible to transform static analyzers with some suitable properties to obtain automatic verification tools based on sufficient verification conditions. We prove that the approach is general and flexible by showing three different verification tools based on different domains of types for functional, logic programming and CLP programming. The verifier for functional programs is obtained from a static analyzer which implements one of the polymorphic type domains introduced by Cousot [Cousot97c]. The one for logic programs is obtained from a static analyzer on a type domain designed by Codish and Lagoon [CodishL98], while the verifier for CLP programs is obtained starting from the type analyzer described in [DrabentP98].}, keywords = {Abstract Interpretation, Abstract Verification, Inductive Verification}, author = {Marco Comini and Roberta Gori and Giorgio Levi}, editor = {Nieuwenhuis, R. and Voronkov, A.} } @proceedings {BagnaraCSZ96, title = {The AND-compositionality of CLP Computed Answer Constraints}, journal = {Proceedings APPIA-GULP-PRODE{\textquoteright}96 Joint Conference on Declarative Programming}, year = {1996}, pages = {355{\textendash}366}, abstract = {We present a semantic characterization of CLP languages for the class of quick-checking systems. We define a semantics of computed answer constraints which is AND-compositional, does not loose the distinction between active and passive constraints in the answers and has both a top-down and a bottom-up characterization. We also show that an incrementality property we impose on the constraint solver is essential in order to define an AND-compositional atom-based semantics.}, author = {Roberto Bagnara and Marco Comini and Francesca Scozzari and Enea Zaffanella}, editor = {Navarro, M.} }