@proceedings {AFJV09a, title = {Defining Datalog in Rewriting Logic}, journal = {Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR{\textquoteright}09)}, volume = {6037}, year = {2010}, pages = {188{\textendash}204}, publisher = {Springer-Verlag}, author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva}, editor = {Schreye, D. de} } @proceedings {BaruzzoC06a, title = {Static Verification of UML Model Consistency}, journal = {MoDeV{$^2$}a: Model Development, Validation and Verification}, year = {2006}, month = {October}, pages = {111{\textendash}126}, publisher = {University of Queensland}, abstract = {UML is nowadays a de-facto standard for design and development of (object-oriented) software. With version 2.0 UML has achieved a more precise formal semantics. The same happened to OCL, a specification language which is an integral part of UML that allows to embed software contracts in the model. In a UML model, different aspects of a system are covered by different types of diagrams and this bears the risk that an overall system specification becomes inconsistent or incomplete. Hence, it is important to provide means to check the consistency and completeness of a UML model. In this work we propose an approach for a static verification of consistency of UML models which relies on OCL constraints. Many approaches for model validation and verification rely on generation of suitable code which dynamically (i.e., at run-time) checks the validity of OCL constraints. This approach has several drawbacks. For example, it cannot generally guarantee that a constraint will never be violated, unless an infinite number of tests is performed. Also the generation of just a significative finite subset is not so feasible because, on one hand, a considerable manual effort is needed even to produce a single test scenario and, on the other hand, test-case generation is well-known to be a hard problem. On the other hand, static approaches based on model checking suffer of the state explosion problem and thus cannot scale to most system sizes. In this paper we propose a static verification technique that, by using OCL constraints together with Class Diagrams, certifies that the dy- namic part of the model is satisfied. This encompasses the weaknesses of the other mentioned methods as it does not require users to build test scenarios and also performs the verification of all system properties at the same time.}, keywords = {OCL, UML diagrams, UML models, Validation, Verification}, url = {http://modeva.itee.uq.edu.au}, author = {Andrea Baruzzo and Marco Comini}, editor = {Hearnden, D. and S{\"u}{\ss}, J. G. and Benoit Baudry and Rapin, N.} } @proceedings {CominiGL00b, title = {Assertion based Inductive Verification Methods for Logic Programs}, journal = {Proceedings of MFCSIT{\textquoteright}2000}, volume = {40}, year = {2001}, note = {Available at URL: {\href{http://www.elsevier.nl/locate/entcs/volume40.html} {\texttt{http://www.elsevier.nl/locate/entcs/volume40.html}}}}, pages = {1{\textendash}18}, publisher = {Elsevier Science Publishers}, abstract = {This paper is an overview of our results on the application of abstract interpretation concepts to the derivation of a verification method for logic programs. These include the systematic design of semantics modeling various proof methods and the characterization of assertions as abstract domains. We first apply the verification framework defined in [CominiGLV99] to derive inductive sufficient conditions for partial correctness. Then the domain of assertions is formalized as an abstract domain. We can therefore derive an assertion based verification method. We finally show two methods based on different assertion languages: a decidable assertion language and Horn clause logic used as assertion language.}, keywords = {Abstract Interpretation, Assertion Language, Inductive Verification, Transformation of logic programs}, author = {Marco Comini and Roberta Gori and Giorgio Levi}, editor = {A. K. Seda} } @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.} }