@proceedings {BacciC10absdiag, title = {Abstract Diagnosis of First Order Functional Logic Programs}, journal = {Logic-based Program Synthesis and Transformation, 20th International Symposium}, volume = {6564}, year = {2011}, pages = {215--233}, publisher = {Springer-Verlag}, address = {Berlin}, abstract = {We present a generic scheme for the abstract debugging of functional logic programs. We associate to programs a semantics based on a (continuous) immediate consequence operator, P[[R]], which models correctly the powerful features of modern functional logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to provide error symptoms in advance and is applicable with partial specifications and even partial programs.}, author = {Giovanni Bacci and Marco Comini}, editor = {Maria Alpuente} } @proceedings {ABER11, title = {Backward Trace Slicing for Rewriting Logic Theories}, journal = {23rd International Conference on Automated Deduction, CADE 23}, year = {2011}, publisher = {Springer}, abstract = {Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commutativity) by means of an algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence the final result. Our methodology is particularly suitable for analyzing complex, textually-large system computations such as those delivered as counter-example traces by Maude model-checkers.}, keywords = {Maude, Rewriting Logic, Trace Slicing}, author = {Maria Alpuente and Demis Ballis and J. Espert and Daniel Omar Romero} } @proceedings {BacciC10absdiag, title = {Abstract Diagnosis of First Order Functional Logic Programs}, journal = {Logic-Based Program Synthesis and Transformation {\textendash} 20th International Symposium {\textendash} Pre-Proceedings}, volume = {10-14}, year = {2010}, pages = {58{\textendash}72}, edition = {20}, address = {Hagenberg, Austria}, abstract = {We present a generic scheme for the abstract debugging of functional-logic programs. We associate to our programs a semantics based on a (continuous) immediate consequence operator, P[[R]], which models correctly the typical cogent features of modern functional-logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness.}, keywords = {Abstract Diagnosis, Debugging, Declarative Diagnosis, Functional-logic Programming}, author = {Giovanni Bacci and Marco Comini}, editor = {Maria Alpuente} } @article {AlpuenteCEFI08, title = {A Compact Fixpoint Semantics for Term Rewriting Systems}, journal = {Theoretical Computer Science}, year = {2010}, note = {To Appear}, abstract = {This work is motivated by the fact that a {\guillemotleft}compact semantics{\guillemotright} for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many {\guillemotleft}semantically useless{\guillemotright} elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation.}, author = {Maria Alpuente and Marco Comini and Santiago Escobar and Moreno Falaschi and Jos{\`e} Iborra} } @proceedings {ABBF11, title = {Completeness of Unfolding for Rewriting Logic Theories}, journal = {12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010}, year = {2010}, pages = {116{\textendash}123}, publisher = {IEEE Computer Society Press}, abstract = {Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowing-based unfolding transformation that is useful to transform rewriting logic theories. We also present a transformation methodology that is able to determine whether an unfolding transformation step would cause incompleteness and avoid this problem by completing the transformed rewrite theory with suitable extra rules. More precisely, our methodology identifies the sources of incompleteness and derives a set of rules that are added to the transformed rewrite theory in order to preserve the semantics of the original theory.}, keywords = {Program Transformation, Rewriting Logic, Unfolding}, author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi} } @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 {ABBF10, title = {A Fold/Unfold Transformation Framework for Rewrite Theories Extended to CCT}, journal = {ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010}, year = {2010}, pages = {43{\textendash}52}, publisher = {Springer}, abstract = {Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we present a fold/unfold-based transformation framework for rewriting logic theories which is based on narrowing. For the best of our knowledge, this is the first fold/unfold transformation framework which allows one to deal with functions, rules, equations, sorts, and algebraic laws (such as commutativity and associativity). We provide correctness results for the transformation system w.r.t. the semantics of ground reducts. Moreover, we show how our transformation technique can be naturally applied to implement a Code Carrying Theory (CCT) system. CCT is an approach for securing delivery of code from a producer to a consumer where only a certificate (usually in the form of assertions and proofs) is transmitted from the producer to the consumer who can check its validity and then extract executable code from it. Within our framework, the certificate consists of a sequence of transformation steps which can be applied to a given consumer specification in order to automatically synthesize safe code in agreement with the original requirements. We also provide an implementation of the program transformation framework in the high-performance, rewriting logic language Maude which, by means of an experimental evaluation of the system, highlights the potentiality of our approach.}, keywords = {CCT, Fold/Unfold Transformations, Program Transformation, Rewriting Logic}, author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi} } @article {ABCF10, title = {An Integrated Framework for the Diagnosis and Correction of Rule-Based Programs}, journal = {Theoretical Computer Science}, volume = {411}, year = {2010}, note = {to appear}, abstract = {We present a generic scheme for the declarative debugging of programs that are written in rewriting-based languages that are equipped with narrowing. Our aim is to provide an integrated development environment in which it is possible to debug a program and then correct it automatically. Our methodology is based on the combination (in a single framework) of a semantics-based diagnoser that identifies those parts of the code that contain errors and an inductive learner that tries to repair them, once the bugs have been located in the program. We develop our methodology in several steps. First, we associate with our programs a semantics that is based on a (continuous) immediate consequence operator, T_R, which models the answers computed by narrowing and is parametric w.r.t. the evaluation strategy, which can be eager or lazy. Then, we show that, given the intended specification of a program R, it is possible to check the correctness of R by a single step of T_R. In order to develop an effective debugging method, we approximate the computed answers semantics of R and derive a finitely terminating bottom-up abstract diagnosis method, which can be used statically. Finally, a bug-correction program synthesis methodology attempts to correct the erroneous components of the wrong code. We propose a hybrid, top-down (unfolding-based) as well as bottom-up (induction-based), correction approach that is driven by a set of evidence examples which are automatically produced as an outcome by the diagnoser. The resulting program is proven to be correct and complete w.r.t. the considered example sets. Our debugging framework does not require the user to provide error symptoms in advance or to answer difficult questions concerning program correctness. An implementation of our debugging system has been undertaken which demonstrates the workability of our approach.}, author = {Maria Alpuente and Demis Ballis and F. Correa and Moreno Falaschi} } @unpublished {ABER10, title = {Model-checking Web Applications with Web-TLR}, journal = {8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010)}, year = {2010}, note = {to appear}, publisher = {Springer}, abstract = {Web-TLR is a software tool designed for model-checking Web applications which is based on rewriting logic. Web applications are expressed as rewrite theories which can be formally verified by using the Maude built-in LTLR model-checker. Web-TLR is equipped with a user-friendly, graphical Web interface that shields the user from unnecessary information. Whenever a property is refuted, an interactive slideshow is generated that allows the user to visually reproduce, step by step, the erroneous navigation trace that underlies the failing model checking computation. This provides deep insight into the system behavior, which helps to debug Web applications.}, keywords = {Model-checking, Rewriting Logic, Verification of Web Applications, Web-TLR}, author = {Maria Alpuente and Demis Ballis and J. Espert and Daniel Omar Romero} } @inbook {ABF10, title = {Transformation and Debugging of Functional Logic Programs}, booktitle = {25 Years GULP 2010}, series = {Lecture Notes in Computer Science}, year = {2010}, pages = {271{\textendash}299}, publisher = {Springer}, organization = {Springer}, chapter = {Transformation and Debugging of Functional Logic Programs}, abstract = {The Italian contribution to functional-logic programming has been significant and influential in a number of areas of semantics, and semantics-based program manipulation techniques. We survey selected topics, with a particular regard to debugging and transformation techniques. These results as usual depend on the narrowing strategy which is adopted and on the properties satisfied by the considered programs. In this paper, we restrict ourselves to first-order functional-logic languages without non-deterministic functions. We start by describing some basic classical transformation techniques, namely folding and unfolding. Then, we recall the narrowing-driven partial evaluation, which is the first generic algorithm for the specialization of functional logic programs. Regarding debugging, we describe a goal-independent approach to automatic diagnosis and correction which applies the immediate consequence operator modeling computed answers to the diagnosis of bugs in functional logic programs. A companion bug-correction program synthesis methodology is described that attempts to correct the erroneous components of the wrong code.}, keywords = {Debugging, Fold/Unfold Transformations, Functional-logic Programming, Program Transformation}, author = {Maria Alpuente and Demis Ballis and Moreno Falaschi} } @article {AFJV09b, title = {DATALOG_SOLVE: A Datalog-Based Demand-Driven Program Analyzer}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {248}, year = {2009}, pages = {57{\textendash}66}, abstract = {This work presents a practical Java program analysis framework that is obtained by combining a Java virtual machine with a general-purpose verification toolbox that we previously extended. In our methodology, Datalog clauses are used to specify complex interprocedural program analyses involving dynamically created objects. After extracting an initial set of Datalog constraints about the Java bytecode program semantics, our framework transforms the Datalog rules of a particular analysis into a Boolean Equation System (Bes), whose local resolution using the aforementioned extended verification toolbox corresponds to the demand- driven computation of the analysis.}, author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva} } @article {AFJV09tr, title = {Defining Datalog in Rewriting Logic}, number = {DSIC-II/07/09}, year = {2009}, publisher = {DSIC, Universidad Polit{\'e}cnica de Valencia}, author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva} } @proceedings {AFJV09, title = {Implementing Datalog in Maude}, journal = {Proceedings of the IX Jornadas sobre Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}09) and I Taller de Programaci{\'o}n Funcional (TPF{\textquoteright}09)}, year = {2009}, month = {September}, pages = {15{\textendash}22}, abstract = {Transformation of programs among different paradigms has been widely studied in academic research and education. The interest on Datalog has recently increased as a specification language for expressing, in just a few lines, complex interprocedural analyses involving dynamically created objects. In real-world problems, the Datalog rules encoding a particular analysis must be solved generally under a huge set of Datalog facts that are automatically extracted from the analyzed program (e.g. pointer dependencies). In that context, this work aims at exploiting Maude{\textquoteright}s capabilities for supporting efficient evaluation of Datalog queries. We demonstrate how, starting from an almost straightforward transformation of Datalog programs into Maude specifications, we are able to achieve a highly efficient version.}, author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva}, editor = {Pe{\~n}a, R.} } @proceedings {ABR09, title = {Specification and Verification of Web Applications in Rewriting Logic}, journal = {16th International Symposium on Formal Methods, FM 2009}, year = {2009}, pages = {790{\textendash}805}, publisher = {Springer}, abstract = {This paper presents a Rewriting Logic framework that formalizes the interactions between Web servers and Web browsers through a communicating protocol abstracting HTTP. The proposed framework includes a scripting language that is powerful enough to model the dynamics of complex Web applications by encompassing the main features of the most popular Web scripting languages (e.g. PHP, ASP, Java Servlets). We also provide a detailed characterization of browser actions (e.g. forward/backward navigation, page refresh, and new window/tab openings) via rewrite rules, and show how our models can be naturally model-checked by using the Linear Temporal Logic of Rewriting (LTLR), which is a Linear Temporal Logic specifically designed for model-checking rewrite theories. Our formalization is particularly suitable for verification purposes, since it allows one to perform in-depth analyses of many subtle aspects related to Web interaction. Finally, the framework has been completely implemented in Maude, and we report on some successful experiments that we conducted by using the Maude LTLR model-checker.}, keywords = {Model-checking, Rewriting Logic, Specification of Web Applications, Verification of Web Applications}, author = {Maria Alpuente and Demis Ballis and Daniel Omar Romero} } @proceedings {AFJV08, title = {Using Datalog and Boolean Equation Systems for Program Analysis}, journal = {Proceedings of the 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS{\textquoteright}08)}, volume = {5596}, year = {2009}, pages = {215{\textendash}231}, publisher = {Springer-Verlag}, abstract = {This paper describes a powerful, fully automated method to evaluate Datalog queries by using Boolean Equation Systems (Bess), and its application to object-oriented program analysis. Datalog is used as a specification language for expressing complex interprocedural program analyses involving dynamically created objects. In our methodology, Datalog rules encoding a particular analysis together with a set of constraints (Datalog facts that are automatically extracted from program source code) are dynamically transformed into a Bes, whose local resolution corresponds to the demand-driven evaluation of the program analysis. This approach allows us to reuse existing general purpose verification toolboxes, such as Cadp, providing local Bes resolutions with linear-time complexity. Our evaluation technique has been implemented and successfully tested on several Java programs and Datalog analyses that demonstrate the feasibility of our approach.}, author = {Maria Alpuente and Marco Antonio Feli{\'u} and Joubert, C. and Alicia Villanueva}, editor = {Darren Cofer and Alessandro Fantechi} } @article {AGPV08, title = {An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source Transformation}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {206}, year = {2008}, pages = {3{\textendash}21}, abstract = {A pretty wide range of concurrent programming languages have been developed over the years. Coming from different programming traditions, concurrent languages differ in many respects, though all share the common aspect to expose parallelism to programmers. In order to provide language level support to programming with more than one process, a few basic concurrency primitives are often combined to provide the main language constructs, sometimes making different assumptions. In this paper, we analyze the most common primitives and related semantics for the class of synchronous concurrent programming languages, i.e., languages with a global mechanism of processes synchronization. Then, we present a generic framework for approximating the semantics of the main constructs which applies to both, declarative as well as imperative concurrent programming languages. We determine the conditions which ensure the correctness of the approximation, so that the resulting abstract semantics safely supports program analysis and verification. Finally, we ascertain the conditions that make it possible to implement the abstraction by a source to source transformation of the language semantics.}, author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva} } @proceedings {ABFOR08, title = {An Abstract Generic Framework for Web Site Verification}, journal = {2008 International Symposium on Applications and the Internet, SAINT 2008}, year = {2008}, pages = {104{\textendash}110}, publisher = {IEEE Computer Society}, abstract = {In this paper, we present an abstract framework for Web site verification which improves the performance of a previous, rewriting-based Web verification methodology. The approximated framework is formalized as a source-to-source transformation which is parametric w.r.t. the chosen abstraction. This transformation significantly reduces the size of the Web documents by dropping or merging contents that do not influence the properties to be checked. This allows us to reuse all verification facilities of the previous system WebVerdi-M to efficiently analyze Web sites. In order to ensure that the verified properties are not affected by the abstraction, we develop a methodology which derives the abstraction of Web sites from their Web specification. We believe that this methodology can be successfully embedded into several frameworks. In particular we have developed a prototypical implementation which shows a huge speedup w.r.t. a previous methodology which did not use this transformation. }, keywords = {Abstract Verification, Web Site Verification, Web-VERDI}, author = {Maria Alpuente and Demis Ballis and Moreno Falaschi and P. Ojeda and Daniel Omar Romero} } @proceedings {CominiDV07, title = {On Polymorphic Recursion, Type Systems, and Abstract Interpretation}, journal = {Static Analysis {\textendash} 15th International Symposium, SAS 2008}, volume = {5079}, year = {2008}, pages = {144{\textendash}158}, publisher = {Springer-Verlag}, address = {Berlin}, abstract = {The problem of typing polymorphic recursion (i.e. recursive function definitions rec{x = e} where different occurrences of x in e are used with different types) has been investigated both by people working on type systems and by people working on abstract interpretation. Recently, Gori and Levi have developed an abstract interpreter that is able to type all the ML typable recursive definitions and interesting examples of polymorphic recursion. The problem of finding a type system corresponding to their abstract interpreter was open. In this paper we present a type system corresponding to the Gori-Levi abstract interpreter. Interestingly enough, the type system is derived from the system of simple types (which is the let-free fragment of the ML type system) by adapting a general technique for extending a decidable type system enjoying principal typings by adding a decidable rule for typing recursive definitions. The key role played in our investigation by the notion of principal typing suggests that this notion might be useful in other investigations about the relations between type systems and type inference algorithms synthesized by abstract interpretation.}, author = {Marco Comini and Ferruccio Damiani and Samuel Vrech}, editor = {Maria Alpuente and Germ{\'a}n Vidal} } @proceedings {ABBF08, title = {Semantic Verification of Web System Contents}, journal = {ER 2008 Workshops (WISM 2008)}, volume = {5232}, year = {2008}, pages = {437{\textendash}446}, publisher = {Springer}, abstract = {In this paper, we present a rule-based specification language to define and automatically check semantic as well as syntactic constraints over the informative content of a Web system. The language is inspired by the GVERDI language and significantly extends it by integrating ontology reasoning into the specification rules and by adding new syntactic constructs. The resulting language increases the expressiveness of the original one and enables a more sophisticated treatment of the semantic information related to the contents of the Web system.}, keywords = {Description logic, OWL, Semantic Verification, Web Site Verification}, author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi} } @proceedings {AGPV07, title = {An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source Transformation}, journal = {Actas de las VII Jornadas de Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}07)}, year = {2007}, month = {sep}, pages = {81{\textendash}92}, abstract = {A pretty wide range of concurrent programming languages have been developed over the years. Coming from different programming traditions, concurrent languages differ in many respects, though all share the common aspect to expose parallelism to programmers. In order to provide language level support to programming with more than one process, a few basic concurrency primitives are often combined to provide the main language constructs, sometimes making different assumptions. In this paper, we analyze the most common primitives and related semantics for the class of synchronous concurrent programming languages, i.e., languages with a global mechanism of processes synchronization. Then, we present a generic framework for approximating the semantics of the main constructs which applies to both, declarative as well as imperative concurrent programming languages. We determine the conditions which ensure the correctness of the approximation, so that the resulting abstract semantics safely supports program analysis and verification. Finally, we ascertain the conditions that make it possible to implement the abstraction by a source to source transformation of the language semantics.}, author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva} } @proceedings {ABFOR07, title = {A Fast Algebraic Web Verification Service}, journal = {Web Reasoning and Rule Systems, 1st International Conference, RR 2007}, volume = {4524}, year = {2007}, publisher = {Springer}, abstract = {In this paper, we present the rewriting-based, Web verification service WebVerdi-M, which is able to recognize forbidden/incorrect patterns and incomplete/missing Web pages. WebVerdi-M relies on a powerful Web verification engine that is written in Maude, which automatically derives the error symptoms. Thanks to the AC pattern matching supported by Maude and its metalevel facilities, WebVerdi-M enjoys much better performance and usability than a previous implementation of the verification framework. By using the XML benchmarking tool xmlgen, we develop some scalable experiments which demonstrate the usefulness of our approach.}, keywords = {Maude, Rewriting Logic, Verification of Web Applications, Web-VERDI}, author = {Maria Alpuente and Demis Ballis and Moreno Falaschi and P. Ojeda and Daniel Omar Romero} } @article {AGV07, title = {A Framework for Timed Concurrent Constraint Programming with External Functions}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {188C}, year = {2007}, pages = {143{\textendash}155}, abstract = {The Timed Concurrent Constraint programming language (tccp in short), was introduced for modeling reactive systems. This language allows one to model in a very intuitive way typical ingredients of these systems such as timeouts, preemptions, etc. However, there is no natural way for modeling other desirable features such as functional computations, for example for calculating arithmetic results. In fact, although it is certainly possible to implement such kind of operations, each single step of the computation takes time in tccp, and avoiding interferences with the intended overall behavior of the (reactive) system is quite involved. In this paper, we propose an extension of tccp for modeling instantaneous computations which improves the expressiveness of the language, in the sense that operations that are cumbersome to implement in pure tccp, are executed by calling an efficient, external functional engine, while the tccp programmer can focus on the pure, and usually more complex, reactive part of the system. We also describe a case study which motivates the work, and discuss how the new capability presented here can also be used as a new tool for developers from the verification point of view.}, keywords = {functions, tccp}, author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva} } @article {AGPV06, title = {A Real-Time Logic for tccp verification}, journal = {Journal of Universal Computer Science}, volume = {12}, number = {11}, year = {2006}, month = {November}, pages = {1551{\textendash}1573}, keywords = {cc, Logic}, author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva} } @article {ABF06, title = {Rule-based Verification of Web Sites}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {8}, number = {6}, year = {2006}, pages = {565{\textendash}585}, abstract = {In this paper, we develop a framework for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are fulfilled. First, we provide a rewriting-based, formal specification language which allows us to define syntactic as well as semantic properties of the Web site. Then, we formalize a verification technique which detects both incorrect/forbidden patterns as well as lack of information, that is, incomplete/missing Web pages, inside the Web site. Useful information is gathered during the verification process which can be used to repair the Web site. Our methodology is based on a novel rewriting-based technique, called {\em partial rewriting}, in which the traditional pattern matching mechanism is replaced by tree simulation, a suitable technique for recognizing patterns inside semistructured documents. The framework has been implemented in the prototype GVerdi, which is publicly available.}, keywords = {GVERDI, Homeomorphic Tree embedding, Tree Simulation, Verification of Web Applications}, author = {Maria Alpuente and Demis Ballis and Moreno Falaschi} } @proceedings {ABFR06, title = {A Semi-Automatic Methodology for Repairing Faulty Web Sites}, journal = {4th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006)}, year = {2006}, pages = {31{\textendash}40}, publisher = {IEEE Computer Society}, abstract = {The development and maintenance of Web sites are difficult tasks. To maintain the consistency of ever-larger, complex Web sites, Web administrators need effective mechanisms that assist them in fixing every possible inconsistency. In this paper, we present a novel methodology for semi-automatically repairing faulty Web sites which can be integrated on top of an existing rewriting-based verification technique developed in a previous work. Starting from a categorization of the kinds of errors that can be found during the Web verification activities, we formulate a stepwise transformation procedure that achieves correctness and completeness of the Web site w.r.t. its formal specification while respecting the structure of the document (e.g. the schema of an XML document). Finally, we shortly describe a prototype implementation of the repairing tool which we used for an experimental evaluation of our method.}, keywords = {Web site debugging, Web site repair}, author = {Maria Alpuente and Demis Ballis and Moreno Falaschi and Daniel Omar Romero} } @article {AGV06-tr, title = {Timed Concurrent Constraint programming with External Functions}, number = {DSIC-II/13/06}, year = {2006}, publisher = {DSIC, UPV}, author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva} } @proceedings {AGV06, title = {Timed Concurrent Constraint Programming with Instantaneous Computations}, journal = {Actas de las VI Jornadas de Programaci}, year = {2006}, address = {Sitges, Barcelona, Spain}, author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva} } @proceedings {ABF05, title = {A Rewriting-based Framework for Web Sites Verification}, journal = {Proceedings of the 5th International Workshop on Rule-Based Programming (RULE 2004)}, year = {2005}, pages = {41{\textendash}61}, publisher = {Elsevier}, abstract = {In this paper, we develop a framework for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are fulfilled. First, we provide a rewriting-based, formal specification language which allows us to define syntactic as well as semantic properties of the Web site. Then, we formalize a verification technique which obtains the requirements not fulfilled by the Web site, and helps to repair the errors by finding out incomplete information and/or missing pages. Our methodology is based on a novel rewriting-based technique, called partial rewriting, in which the traditional pattern matching mechanism is replaced by tree simulation, a suitable technique for recognizing patterns inside semistructured documents. The framework has been implemented in the prototype Web verification system Verdi which is publicly available.}, keywords = {partial rewriting, Tree Simulation, VERDI, verification of Web sites}, author = {Maria Alpuente and Demis Ballis and Moreno Falaschi} } @article {AGPV05, title = {A Semantic Framework for the Abstract Model Checking of tccp programs}, journal = {{Theoretical Computer Science}}, volume = {346}, year = {2005}, pages = {58{\textendash}95}, keywords = {Abstraction, cc, model checking}, author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva} } @inbook {AFV04, title = {A Symbolic Model checker for tccp Programs}, booktitle = {Proceedings of the International Workshop on Rapid Integration of Software Ingeneering techniques (RISE{\textquoteright}04)}, series = {Lecture Notes in Computer Science}, volume = {3475}, year = {2005}, pages = {45{\textendash}56}, publisher = {Springer Verlag}, organization = {Springer Verlag}, keywords = {cc, model checking, symbolic representation}, author = {Maria Alpuente and Moreno Falaschi and Alicia Villanueva} } @proceedings {AGPV05c, title = {Verifying Real-Time Properties of tccp Programs}, journal = {Proc. of the Quintas Jornadas sobre Programaci{\'o}n y Lenguajes, PROLE{\textquoteright}05, 2005}, year = {2005}, pages = {85{\textendash}94}, author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}, editor = {L{\'o}pez-Fraguas, F.J.} } @article {AGPV04, title = {Abstract Model Checking of tccp programs}, journal = {Electronic Notes in Theoretical Computer Science (ENTCS)}, volume = {112}, year = {2004}, pages = {19{\textendash}36}, keywords = {Abstraction, cc, model checking}, author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva} } @proceedings {ABF04b, title = {An Automated Tool for Web Sites Verification}, journal = {Logics in Artificial Intelligence, 9th European Conference, JELIA 2004}, volume = {3229}, year = {2004}, pages = {726{\textendash}729}, publisher = {Springer}, author = {Maria Alpuente and Demis Ballis and Moreno Falaschi} } @proceedings {ABF04a, title = {Automated Verification of Web Sites Using Partial Rewriting}, journal = {Pre-Proceedings of the 1st International Symposium on Leveraging Applications of Formal Methods, ISoLA 2004}, year = {2004}, pages = {81{\textendash}88}, author = {Maria Alpuente and Demis Ballis and Moreno Falaschi} } @proceedings {ABEFL03b, title = {Abstract Correction of First-Order Functional Programs}, journal = {12th International Workshop on Functional and Constraint Logic Programming, WFLP 2003}, volume = {86}, number = {3}, year = {2003}, publisher = {Elsevier}, abstract = {Debussy is an (abstract) declarative diagnosis tool for functional programs which are written in OBJ style. The debugger does not require the user to either provide error symptoms in advance or answer any question concerning program correctness. In this paper, we formalize an inductive learning methodology for repairing program bugs in OBJ-like programs. Correct program rules are automatically synthesized from examples which might be generated as an outcome by the Debussy diagnoser.}, keywords = {Debugging, Inductive Learning, OBJ, program correction}, author = {Maria Alpuente and Demis Ballis and Santiago Escobar and Moreno Falaschi and Salvador Lucas} } @proceedings {ABEFL03a, title = {Abstract Correction of OBJ-like Programs}, journal = {Informl Proceeding of APPIA GULP PRODE 2003 (AGP 2003)}, year = {2003}, pages = {422{\textendash}433}, author = {Maria Alpuente and Demis Ballis and Santiago Escobar and Moreno Falaschi and Salvador Lucas} } @proceedings {AlpuenteCEFL02, title = {Abstract Diagnosis of Functional Programs}, journal = {Logic Based Program Synthesis and Tranformation {\textendash} 12th International Workshop, LOPSTR 2002, Revised Selected Papers}, volume = {2664}, year = {2003}, publisher = {Springer-Verlag}, address = {Berlin}, abstract = {We present a generic scheme for the declarative debugging of functional programs modeled as (conditional) term rewriting systems. We associate to our programs a semantics based on a (continuous) immediate consequence operator, TR, which models the (values/normal forms) semantics of R. Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness. We have made available a prototypical implementation in Haskell and have tested it on some non trivial examples.}, keywords = {Abstract Diagnosis, Abstract Interpretation, Abstract Verification, Declarative Debugging, Functional Programming, Inductive Verification}, author = {Maria Alpuente and Marco Comini and Santiago Escobar and Moreno Falaschi and Salvador Lucas}, editor = {Leuschel, M.} } @proceedings {ABCF03, title = {Correction of Functional Logic Programs}, journal = {Programming Languages and Systems, 12th European Symposium on Programming, ESOP 2003}, volume = {2618}, year = {2003}, pages = {54{\textendash}68}, publisher = {Springer}, abstract = {We propose a new methodology for synthesizing correct functional logic programs. We aim to create an integrated development environment in which it is possible to debug a program and correct it automatically. We start from a declarative diagnoser that we have developed previously which allows us to identify wrong program rules w.r.t. an intended specification. Then a bug-correction, program synthesis methodology tries to correct the erroneous components of the wrong code. We propose a hybrid, top-down (unfolding-based) as well as bottom-up (induction-based), approach for the automatic correction of functional logic programs which is driven by a set of evidence examples which are automatically produced as an outcome by the diagnoser. The resulting program is proven to be correct and complete w.r.t. the considered example sets. Finally, we also provide a prototypical implementation which we use for an experimental evaluation of our system. }, keywords = {Debugging, Functional-logic Programming, program correction, Program Transformation, Unfolding}, author = {Maria Alpuente and Demis Ballis and F. Correa and Moreno Falaschi} } @proceedings {AFV03b, title = {Symbolic Model Checking for Timed Concurrent Constraint Programs}, journal = {Proceedings of the III Jornadas de Programaci{\'o}n y Lenguajes}, year = {2003}, address = {Alicante}, keywords = {cc, model checking, symbolic representation}, author = {Maria Alpuente and Moreno Falaschi and Alicia Villanueva} } @proceedings {ABCF02, title = {A Multiparadigm Automatic Correction Scheme}, journal = {Pre-Proceedings of the 11th International Workshop on Functional and (Constraint) Logic Programming, WFLP 2002}, year = {2002}, author = {Maria Alpuente and Demis Ballis and F. Correa and Moreno Falaschi} }