A conditional slicing tool for Maude

Escola Tècnica Superior d’Enginyeria Informàtica Universitat Politècnica de València A Conditional Slicing Tool for Maude Final Year Project Ingeniería Informática Author: Julia Sapiña Sanchis Supervisors: María Alpuente Frasnedo Francisco Frechina Navarro Valencia, September 2012 Abstract In this work we develop Julienne, an online trace slicer for the high performance rewriting logic language Maude. Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and comprehension. Our slicing tool allows us to systematically trace back reverse dependences and causality along Maude computation traces by means of an algorithm that dynamically simplifies the trace and elides useless data that do not influence the final result. We describe the main facilities provided by the tool as well as the features and architecture of the tool. The tool is particularly suitable for analyzing complex, textually large execution traces such as those delivered by Maude model checkers. 2 Keywords Slicing, Rewriting Logic, Maude, Julienne. 3 Contents Introduction 9 1 Slicing 11 1.1 WhatisSlicing?.......................... 11 1.2 TypesofSlicing.......................... 12 1.2.1 Backward Trace Slicing . . . . . . . . . . . . . . . . . . 13 1.2.2 Incremental Slicing . . . . . . . . . . . . . . . . . . . . 14 2Julienne Online Trace Slicer 15 2.1 Providing the Maude Specification . . . . . . . . . . . . . . . . 15 2.2 Providing the Execution Trace . . . . . . . . . . . . . . . . . . 15 2.3 Navigating through the Trace . . . . . . . . . . . . . . . . . . 16 2.4 Specifying the Slicing Criterion . . . . . . . . . . . . . . . . . 17 2.5 Performing the Slice . . . . . . . . . . . . . . . . . . . . . . . 18 2.6 Trace Slice Results . . . . . . . . . . . . . . . . . . . . . . . . 19 3 Implementation 22 3.1 Technologies............................ 22 3.1.1 Maude........................... 22 3.1.2 HyperText Mark-up Language . . . . . . . . . . . . . . 23 3.1.3 Cascading Style Sheets . . . . . . . . . . . . . . . . . . 23 3.1.4 JavaScript ........................ 24 3.2 Implementation Details . . . . . . . . . . . . . . . . . . . . . . 25 3.2.1 Graphical User Interface . . . . . . . . . . . . . . . . . 25 3.2.1.1 General Decisions . . . . . . . . . . . . . . . . 25 3.2.1.2 Slider ...................... 26 3.2.1.3 Hiding Irrelevant Data . . . . . . . . . . . . . 26 3.2.2 Selecting the Slicing Criterion . . . . . . . . . . . . . . 27 3.2.2.1 Subterm position . . . . . . . . . . . . . . . . 28 3.2.2.2 Common technical details . . . . . . . . . . . 29 3.2.2.3 Meta-level representation . . . . . . . . . . . 30 3.2.2.4 Source-level representation . . . . . . . . . . . 31 4 Contents 5 3.2.2.5 State Map Structure . . . . . . . . . . . . . . 32 4 Using Julienne 35 4.1 Crossing River Example . . . . . . . . . . . . . . . . . . . . . 35 4.2 BankExample........................... 40 Conclusions and Future Work 47 Bibliography 48 List of Figures 2.1 Julienne showing a list of predefined examples and loading the Bank with error example specification. . . . . . . . . . . . 16 2.2 Maude execution trace loaded in Julienne. .......... 17 2.3 Generation of a Maude execution trace by providing both the initial and final state. . . . . . . . . . . . . . . . . . . . . . . . 18 2.4 Julienne flashing in red and alerting the user about a possible mistake in the provided information. . . . . . . . . . . . . . . 19 2.5 Information displayed (in source-level representation) after pressing state transition arrow. . . . . . . . . . . . . . . . . . . . . 20 2.6 Slicing criteria fixed in the states 20 and 21 of the execution trace................................. 20 2.7 Result obtained after applying the backward-slicing technique with the slicing criterion described in Figure 2.6. . . . . . . . . 21 3.1 Original versus sliced trace. . . . . . . . . . . . . . . . . . . . 27 3.2 Position tree of a state expressed in meta-level representation. 29 3.3 Position tree of a state expressed in source-level representation. 30 4.1 Julienne showing a specification of the crossing river example. 36 4.2 Generation of a Maude execution trace by providing the initial and final state in source-level representation. . . . . . . . . . . 37 4.3 A Maude execution trace of 56 states with a selected slicing criterion in the last state. . . . . . . . . . . . . . . . . . . . . . 37 4.4 Original and sliced trace states after applying the backwardslicing technique with the slicing criterion described in Figure 4.3.................................. 38 4.5 Sliced trace showing a reduction of 77% with respect to the original execution trace. . . . . . . . . . . . . . . . . . . . . . 39 4.6 Julienne showing a Maude bank specification with an error inoneofitsrules.......................... 40 4.7 Execution trace provided as an example for the faulty Bank specification............................. 41 6 List of Figures 7 4.8 A 22 state execution trace of the faulty Bank specification with the minus symbol selected as the slicing criterion. . . . . 42 4.9 Snapshot of the tool after applying the backward-slicing techniqueinFigure4.8......................... 43 4.10 Original versus sliced trace for the Bank example. . . . . . . . 44 4.11 States 8 and 9 of the execution trace displayed in Figure 4.9 with a slicing criterion specified in state 9. . . . . . . . . . . . 45 4.12 Snapshot of Julienne after applying the backward-slicing technique in Figure 4.11. . . . . . . . . . . . . . . . . . . . . . 45 4.13 Table of results of Figure 4.12. . . . . . . . . . . . . . . . . . . 46 List of Tables 3.1 Breakdown of a map by elements and their correspondence with the associated state. . . . . . . . . . . . . . . . . . . . . . 33 8 Chapter 2 Julienne Online Trace Slicer Julienne [1] is an online trace slicer tool developed by members of the Extensions of Logic Programming (ELP) research group at the Department of Information System and Computation inside the Universitat Politècnica de València. The first version of this tool allowed to apply the backwardslicing technique [4] in order to slice Maude execution traces. The new and extended version of the tool developed in the current project adds some useful features without neglecting the previous existing ones. The new features can be classified in two major categories, those oriented to ease the task of slicing to the user, that is, improving the usability of the tool, and those adding some advanced functionality. The following sections explain in detail the use, features and implementation of the new tool Julienne. 2.1 Providing the Maude Specification The first step while using Julienne is to provide the Maude specification that will be used in the subsequent steps. The user has the choice of either provide a new, custom specification or selecting one of the examples that Julienne provides for evaluation purposes, which will be copied automatically in the text input area as it is selected. 2.2 Providing the Execution Trace After providing the specification, the next step is to provide a valid execution trace. If the user has previously selected one of the given examples as input specification, there will be one execution trace already loaded that, of course, can be replaced if desired. If not, there are two ways to provide it. The first way is to copy a valid (i.e., with no syntax errors and related to the previously provided specification) execution trace. The second way is use the trace generator with which Julienne is endowed by specifying two valid states, initial and final, of the desired execution trace. Julienne trace 15 Chapter 2. Julienne Online Trace Slicer 16 Figure 2.1: Julienne showing a list of predefined examples and loading the Bank with error example specification. generator will find, if it is possible, one execution trace that leads from the given initial state to the final one. This last way of obtaining an execution trace by means of the trace generator can be done by giving the states either at the meta-level or source-level representation. At this point, an error can arise because of a mistake in the provided specification, provided states, execution trace, or because there is no path leading from the given initial state to the final one. In case of error, the corresponding input text area will flash in red and a proper message will alert the user as shown in Figure 2.4. 2.3 Navigating through the Trace Once the user has provided a valid specification and execution trace, Julienne will show in a slider all the states of the trace, from the first to the last one, offering the possibility of viewing the information also in sourcelevel or meta-level representation. This way, the user can visit any state by using the navigation buttons or by specifying a particular state and pressing Chapter 2. Julienne Online Trace Slicer 17 Figure 2.2: Maude execution trace loaded in Julienne. the Go button. Then, the user can select the slicing criterion in any of the states, not only in the last state. In addition, by pressing the arrow that symbolizes the transition between states, Julienne displays useful information about that particular transition, as shown in Figure 2.5. 2.4 Specifying the Slicing Criterion The next step in our methodology is to specify the desired slicing criterion. This task can be performed by highlighting with the mouse any part of the considered relevant text of any state with the exception, of course, of the first one, as it does not have any previous state and the slicing is performed backwards. The user can select as many criteria as she wants in any of the states but only those selected in the earliest state will be considered as the slicing criterion. For example, if Julienne shows an execution trace of 22 states like the one in Figure 2.6 and the user selects some text in states 5, 10 and 20, the slicing criterion will be retrieved from the 5th state. Also, while selecting the slicing criterion, the user can left-click any se- Chapter 2. Julienne Online Trace Slicer 18 Figure 2.3: Generation of a Maude execution trace by providing both the initial and final state. lected text to remove the highlighting or just select the Clear slicing criterion button, which will remove all the slicing criteria previously specified. 2.5 Performing the Slice After specifying the slicing criterion, the backward-slicing technique is applied and the delivered sliced trace will be displayed together with the original trace up to the state where the slicing process started to be applied. That means that, if the execution trace has 22 states and the user selects a slicing criterion in the 20th state, the new trace will only have the first 20 states. However, if the user feels that the criterion was useless or wants to specify a different one, just by selecting the Restore original trace button, the original trace will be fully restored as expected. At this point, the user has the possibility of either restore the full original trace and perform another different slice or slice even more the current sliced trace in the same way the original trace was sliced to remove further unnecessary information. This is what we refer with incremental slicing and Chapter 2. Julienne Online Trace Slicer 19 Figure 2.4: Julienne flashing in red and alerting the user about a possible mistake in the provided information. will be shown in more detail in Section 4.2. Additionally, another useful feature that is only available when a sliced trace is displayed is the possibility of partially hide irrelevant information by means of the Hide irrelevant data checkbox. 2.6 Trace Slice Results Each time a slice is performed, by selecting the Show trace slice button, the user can access to a table that contains all the information of the slicing process, that is, the number of steps, the rule applied at each step, the original trace and the sliced trace. This information can be displayed in either sourcelevel or meta-level representation and, in both representations, the irrelevant information can be partially hidden by means of the Hide irrelevant data checkbox, a feature that is also available while navigating the sliced trace. Chapter 2. Julienne Online Trace Slicer 20 Figure 2.5: Information displayed (in source-level representation) after pressing state transition arrow. Figure 2.6: Slicing criteria fixed in the states 20 and 21 of the execution trace. Chapter 2. Julienne Online Trace Slicer 21 Figure 2.7: Result obtained after applying the backward-slicing technique with the slicing criterion described in Figure 2.6. Chapter 3 Implementation 3.1 Technologies In this section we briefly comment the different technologies that we have used to develop Julienne. 3.1.1 Maude Maude is a high-performance reflective language and system created by José Meseguer at the Stanford Research Institute International (SRI International) and licensed under the terms of the GNU General Public License. The official version is currently being developed by an international team [8] of researchers, although any user can access and modify its source code. Usually, the modifications are given in the form of separate modules which can be included by means of a key word. Some of the principal characteristics of Maude described in [16] are the following: •Based on rewriting logic. •Wide-spectrum. •Multiparadigm. •Reflective. •Internal Strategies. In our tool, Maude plays a key role since it is the language we also used to implement the backward-slicing technique described in [4], as well as generate the state maps and the encoded messages that contain the results to be delivered from the Maude system to Julienne. The first version of our tool had all the developed Maude code contained in an ad hoc module named ConditionalSlicing. This second version of the tool slightly modifies this module and has all the new developed code in a new 22 Chapter 3. Implementation 23 different module named Julienne, which also includes the ConditionalSlicing module, as it makes use of it. 3.1.2 HyperText Mark-up Language The HyperText Mark-up Language (HTML) is a mark-up language created in 1990 by Tim Berners-Lee at the Conseil Européen pour la Recherche Nucléaire (CERN), shortly after establishing [14] the bases for the HyperText Transfer Protocol (HTTP) and therefore the World Wide Web. In October of 1994, Berners-Lee founded the World Wide Web Consortium (W3C), in order to coordinate the efforts to continue developing, maintaining and extending this language. Currently, the W3C foundation is responsible for developing and publishing the standards of this language. In January of 2008 the last version of the standard, HTML5, was published as a working draft and it is expected to be fully developed by 2014, although nowadays almost all browsers support it entirely. Being an online tool, Julienne is developed using HTML in collaboration with other languages. In particular, HTML was used to create the bases of the interface, whose appearance and behaviour where modified later by means of CSS and JavaScript, respectively. We focused on extending a previous version of the tool as well as adapting it to the last version of the HTML standard, HTML5. The primary reasons to such decision were to offer the same experience to the user regardless of the browser that is being used and to extend the life of the code as much as possible. 3.1.3 Cascading Style Sheets Cascading Style Sheets (CSS) is a style sheet language created [15] in 1994 by Håkon Wium Lie, also at CERN. The primary purpose of this language is to cover a gap intentionally left by HTML with respect to styling documents in order to achieve different visual representations of a document without modifying it and only associating a style sheet. Being closely related to HTML, CSS standards are developed and published by the same organization as HTML, the W3C. At the present time, the last fully developed version available is CSS3, although since September 29, 2009, a new draft for CSS4 was started. However, unlike the HTML5 standard, which is fully supported by all major browsers despite not being completely developed, CSS4 is not yet supported by any of them, so we chose to use the CSS3 standard in our tool. In Julienne, CSS3 was used to configure the appearance of all elements of the GUI, that is, specifying their size, font, color, position, margins, ... Chapter 3. Implementation 24 etc. This was achieved following two different strategies. The first strategy is useful to specify the style information of highly customized elements and consists in specifying all the desired rules directly for the element. The second strategy is useful when different elements share the same values of attributes; for example background color or image, line widths, ... etc. In order to specify the value of those attributes, instead of repeating each rule for each element, CSS3 allows all the desired rules to be grouped within a class and then associate the class to any number of elements. An HTML element can have many associated classes and thus benefit from all of them. In case of conflict, that is, an element has associated two classes which specify different values for the same attribute, the browser will determine the most specific rule and apply it. Furthermore, this second strategy is ideal for changing the visual appearance of elements dynamically, that is, we can associate and detach previously specified classes to an element by means of JavaScript in response to any user interaction. 3.1.4 JavaScript JavaScript is a scripting language formalized in the ECMAScript language standardized by Ecma International - European Association for Standardizing Information and Communication Systems, founded in 1961, in the ECMA-262 specification and ISO/IEC 16262. Currently, the most recent revision of the ECMA-262 standard specification is v. 5.1, published in June 2011. Despite of its name, JavaScript is not an evolution from the Java language, although it is influenced by it in terms of naming conventions. In fact, JavaScript is influenced by languages C, Java, Perl and Python and even though it has its utility outside the web environment, it is there where shows its full potential. In Julienne, JavaScript is used client-side to implement all the behaviour of the tool except for the calculations related to the application of the backward-slicing technique and generations of state maps. This behaviour ranges from the very simple task of highlighting one button when the mouse is over it to the most complicated task of decryption of a state map and the subsequent calculus of the position of the slicing criterion. The following list contains some significant features of the tool that were implemented by using JavaScript: •The slider displaying the states of an execution trace. •All the animations between steps in the tool. Chapter 3. Implementation 31 each relevant position, which are those found while reading between an open span tag and its corresponding close tag. The result will be an array of relevant positions to be provided directly to the backward-slicing operator in Maude. 3.2.2.4 Source-level representation While the meta-level representation had a very distinctive pattern that is common to all possible states, regardless of their specifications, a source-level representation did not have any. This was the main problem to solve, not only in this section, but in the entire new version of the tool. One of the beauties of Maude is that it provides the means for the user to create complex models whose states can be represented in many, many forms, often limited by his imagination. This makes literally impossible to find a pattern common to all these possible states. Nevertheless, with our approach, this can be easily solved. At this point, we need to explain that a source-level representation of a state in Julienne is the result of a custom Maude operation, dt, named for downTerm, whose main goal is to lower a given state in meta-level representation from the meta-level to the source-level. This operator dt recursively builds the state in source-level representation by translating each term step by step according to the Maude specification provided, and placing them in the correct order. Once we know how a source-level representation of a state is built, we can easily think that, besides translating each term into its source-level representation, we can translate it into any kind of information that will help us to find the position of any character of the state, that is, we can write the information needed to create a map of the state. Also, with regard to the efficiency of this process, both the calculation of the position of each term and the building of the map can be performed in parallel with the generation of the source-level representation state while using dt, as all three functions run throughout the text in the same recursively manner. With this new information, the formerly very complicated task of finding the positions of the selected terms is greatly eased. First of all, we do not need the information of the state anymore, nor we need to have any semantic knowledge of it. We only need the indices of the selected text inside the string that represents it. The easiest way of obtaining this is to create a mask of the state by replacing any found character, spaces included, with, for example, “n” if it is not wrapped inside a span tag and “S” if it is. Then, we only have to read the map sequentially. As explained in Section 3.2.2.5, each element of the map contains two Chapter 3. Implementation 32 data. The first one describes how many characters the second data will affect. This second data just describes the position of those characters. Once we read an element of the map, we can easily get a substring of the mask starting at the current value of the pointer used to read, and with the length given by the value of the first data of the read element. Then, if this substring contains the character “S”, the position of the term is included in the result array of positions. At the end, just by building the map, the algorithm that is able to get the positions of the terms is even simpler than the used for meta-level representation. 3.2.2.5 State Map Structure As mentioned in Section 3.2.2.4, in order to retrieve the slicing criterion specified by the user in the source representation of a state, it is useful to construct a map of it. The fact that Julienne allows the slicing criterion to be fixed in any state of the execution trace except for the first one implies that all those states need to be mapped. Being Julienne an online web application, the server hosting our tool needs to deliver this information, along with the two representations of each state, to the user, so the size of all this new generated information needs to be lightened as much as possible, as it is affected by the considered Maude specification and the number of states of the execution trace, which can be huge. The positive side is that this operation only needs to be performed once per execution trace provided, regardless of the number of slices later required by the user. The minimum information needed to retrieve a position of a term inside a state is both its position according to the string of characters that represents that state and its position according to the tree of positions described in Section 3.2.2.1. For example, given the bank specification described in Section 4.2 and this state in meta-level representation: ’_;_[’debit[’Alice.Id,’s_^30[’0.Zero]],’_;_[’<_|_>[’Alice .Id,’s_^100[’0.Zero]],’credit[’Alice.Id,’s_^50[’0.Zero]]]] The result of calling the dt operator with them as arguments will be: debit(Alice,30) ; < Alice | 100 > ; credit(Alice,50) and the generated map will be: c6p.1c5p.1.1c1p.1c2p.1.2X.1.2.1c1p.1c3pc2p.2.1c5p.2.1.1 c3p.2.1c3p.2.1.2X.2.1.2.1c2p.2.1c3p.2c7p.2.2c5p.2.2.1 c1p.2.2c2p.2.2.2X.2.2.2.1c1p.2.2 Chapter 3. Implementation 33 Let us explain these results. First, the map is a sequence of concatenated elements each consisting of two data components. The first component begins with the ccharacter and describes how many characters will affect the second data. This second data begins with the pcharacter and describes the position of those characters according with the tree of positions explained in Section 3.2.2.1. Moreover, it is possible that two terms in meta-level representation will merge into one single joint representation. This happens with the natural numbers, as their meta-level representation comprises two related terms (e.g. ’s_ˆX[’0.Zero], being Xa given number). In order to cover those cases, the second data of an element can describe more than one position and thus need to be delimited, in our case with the Xcharacter. Finally, since the root of the tree of positions is always Lambda, it is implicit and does not need to be reflected in the map, so an empty second component can be given, meaning that the position is λitself. Map element Length Characters Positions c6p.1 6 debit( λ.1 c5p.1.1 5 Alice λ.1.1 c1p.1 1 , λ.1 c2p.1.2X.1.2.1 2 30 λ.1.2, λ.1.2.1 c1p.1 1 ) λ.1 c3p 3 _;_ λ c2p.2.1 2 <_ λ.2.1 c5p.2.1.1 5 Alice λ.2.1.1 c3p.2.1 3 _|_ λ.2.1 c3p.2.1.2X.2.1.2.1 3 100 λ.2.1.2, λ.2.1.2.1 c2p.2.1 2 _> λ.2.1 c3p.2 3 _;_ λ.2 c7p.2.2 7 credit( λ.2.2 c5p.2.2.1 5 Alice λ.2.2.1 c1p.2.2 1 , λ.2.2 c2p.2.2.2X.2.2.2.1 2 50 λ.2.2.2, λ.2.2.2.1 c1p.2.2 1 ) λ.2.2 Table 3.1: Breakdown of a map by elements and their correspondence with the associated state. With all this in mind, going back to our example, the first element will be c6p.1. This means that the first six characters of the source-level repre- Chapter 3. Implementation 34 sentation of the state will correspond to the λ.1 position, that is, "debit(". The next element of the map is c5p.1.1, which means that the next five characters, "Alice", will be part of the term with position λ.1.1. And so the map is read sequentially together with the source-level representation of the state. Chapter 4 Using Julienne 4.1 Crossing River Example The simplest example provided for evaluation purposes in the Julienne distribution package is the well-known problem of the crossing river. One of the many variants of the statement of this problem is as follows: There is a man, a wolf, a goat and a cabbage in one side of a river that need to cross to the other side by means of a boat. The boat can only accommodate one traveller besides the man, but leaving the wolf and the goat together without his supervision will cause the wolf to eat the goat and so leaving the goat with the cabbage. First of all, we have to load the corresponding specification by selecting the crossing-river example as shown in Figure 4.1. The next step is to provide a valid execution trace. In this example, instead of using the default execution trace provided by Julienne, we generate a different trace by providing both initial and final states in source-level representation. Our initial state will correspond to the state with all four passengers standing at the left side of the river and our final state will be that with them safely carried to the opposite side. By pressing the Generate trace button, Julienne will generate one of the possible solutions to this problem and will display it as the provided execution trace. Now, we press the Next button to start slicing. As Figure 4.3 shows, the previously generated execution trace has 56 states. We now chose as the slicing criterion the term of the last state describing the side of the river that the wolf is at, that is, right. After pressing the Slice button, the sliced trace states will be displayed along with the original trace states, as Figure 4.4 shows. We can observe that many sliced states are marked with the ***deleted*** text. This means that the state is substantially the same as the preceding one and can be safely omitted. 35 Chapter 4. Using Julienne 36 Finally, by pressing the Show trace slice button, we can consult all the information in a condensed table, along with some additional data about the reduction achieved, which in this example is 77% of the original trace (Figure 4.5). Figure 4.1: Julienne showing a specification of the crossing river example. Chapter 4. Using Julienne 37 Figure 4.2: Generation of a Maude execution trace by providing the initial and final state in source-level representation. Figure 4.3: A Maude execution trace of 56 states with a selected slicing criterion in the last state. Chapter 4. Using Julienne 38 Figure 4.4: Original and sliced trace states after applying the backwardslicing technique with the slicing criterion described in Figure 4.3. Chapter 4. Using Julienne 39 Figure 4.5: Sliced trace showing a reduction of 77% with respect to the original execution trace. Chapter 4. Using Julienne 40 4.2 Bank Example In this second example, also provided within the Julienne distribution package, we work with a very basic Maude specification of a bank system. There are three basic rules, credit,debitERR and transfer. Obviously by its name, the rule labelled as debitERR is introduced to illustrate some problems. Figure 4.6: Julienne showing a Maude bank specification with an error in one of its rules. The first rule, credit, adds some amount of money to a bank account. The second rule, debitERR subtracts it, as if we charge the account with any amount of money, and the transfer rule just moves some money from an account to another one. As we will discover later, the problem is that the debitERR does not check if there is enough money to be withdrawn from the given account. Once we load the specification, we press the Next button and get a default execution trace also provided by Julienne. As this trace is affected by the error we want to discover, we just press Next again to move forward to the trace navigation step. Conclusions and Future Work In this project, we have developed a tool for slicing execution traces delivered by Maude. In order to achieve better reduction rates in the sliced execution traces, apart from the chosen slicing technique that we apply, we focus on aspects that are crucial for the slicing effectiveness: to provide a suitable slicing criterion and the state of the trace in which the slicing technique will be applied. To improve the accuracy of the slicing criterion, which is typically provided by the user, we endow Julienne with a graphical facility that simplifies the process of identifying and fixing it. Moreover, by allowing the slicing technique to be applied in any state of the provided execution trace, Julienne offers to the user the possibility to apply the slicing technique in an incremental way and even change the slicing criterion for each application. The new version of Julienne offers solutions to both problems and provides the user with a very friendly working environment to get the best possible results. As possible future work, we plan to integrate Julienne with an incremental debugger for Maude which uses backward trace slicing to improve the debugging experience. 47 Bibliography [1] Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Julienne: a Trace Slicer for Conditional Rewrite Theories. In: Proc. FM 2012. Springer LNCS 7436: 28–32 (2012) [2] Alpuente, M., Ballis, D., Espert, J., Romero, D.: Model-checking Web Applications with Web-TLR. In: Proc. ATVA 2010. Springer LNCS 6252: 341–346 (2010) [3] Alpuente, M., Ballis, D., Espert, J., Romero, D.: Backward Trace Slicing for Rewriting Logic Theories. In: Proc. CADE 2011. Springer LNCS 6803: 34–48 (2011) [4] Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Backward Trace Slicing for Conditional Rewrite Theories. In: Proc. LPAR-18. Springer LNCS 7180: 62–76 (2012) [5] Alpuente, M., Ballis, D., Romero, D.: Specification and Verification of Web Applications in Rewriting Logic. In: Proc. FM 2009. Springer LNCS 5850: 790–805 (2009) [6] Baggi, M., Ballis, D., Falaschi, M.: Quantitative Pathway Logic for Computational Biology. In: Proc. CMSB ’09. Springer LNCS 5688: 68– 82 (2009) [7] Chen, F., Rosu, G.: Parametric Trace Slicing and Monitoring. In: TACAS. Springer LNCS 5505: 246–261 (2009) [8] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.6): [9] Clavel, M., Durán, F., Hendrix, J., Lucas, S., Meseguer, J., Ölveczky, P.C.: The Maude Formal Tool Environment. In: Proc. CALCO. Springer LNCS 4624: 173–178 (2007) [10] The julienne Web site (2012), available at: http://users.dsic.upv.es/grupos/elp/soft.html 48 Bibliography 49 [11] The julienne v. 2 Web site (2012), available at: http://safe-tools.dsic.upv.es/julienneV2 [12] TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge, UK (2003) [13] Martí-Oliet, N., Palomino, M., Verdejo, A.: Rewriting logic bibliography by topic: 1990-2011. Journal of Logic and Algebraic Programming. To appear (2012) [14] Berners-Lee, T. Information Management: A Proposal. [15] Lie, H. W. Cascading HTML Style Sheets: A Proposal. [16] Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. Electronic Notes in Theoretical Computer Science, Vol. 4: 65–89 (1996) [17] Gallagher, K., Binkley, D.: Program Slicing. Advances in Computers, Vol. 43: 1–50 (1996) [18] Silva, J.: A Vocabulary of Program Slicing-Based Techniques. In: ACM Comput. Surv. 44, 3. Article 12 (June 2012).