ResumenMakina: A New QuickCheck State Machine LibraryBueso de Barrio, Luis Eduardo; Fredlund, Lars-Ake; Herranz, Angel; Benac Earle, Clara; Mariño, Julio. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.This article presents Makina, a new library and a domain specific language for writing property-based testing models for stateful programs. Models written in the new domain specific language are, using Elixir macros, rewritten into normal QuickCheck state machines. Our main goals with Makina are to facilitate the task of developing correct and maintainable models, and to encourage model reuse. To meet these goals, Makina provides a declarative syntax for defin- ing model states and model commands. In particular, Makina encourages the typing of specifications, and ensures through its rewrite rules that such type information can be used by, e.g., the Dialyzer tool, to effectively typecheck models. More- over, to promote model reuse, the domain specific language provides constructs to permit models to be defined in terms of collections of previously defined models. ResumenFine-grained Graph Representation for Program SlicingGalindo, Carlos; Pérez Rubio, Sergio; Sílva, Josep. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.The system dependence graph (SDG) is the standard program representation used for program slicing, a technique that computes the SDG from the source code to explore the parts of a program that affect or are affected by an arbitrarily selected program point called slicing criterion. This paper shows how the representation provided by the SDG is imprecise when representing some program structures, demanding modifications to accurately apply program slicing over them, and we introduce an extension of the SDG to deal with all these representation problems in a natural way. This extension is called the expression dependence graph (EDG). The EDG extends the SDG by changing the granularity of its nodes to abstract syntax tree (AST) nodes. The new decomposed program representation leads to the definition of new program dependences that appear when breaking down statements into multiple nodes, and provides the potential of selecting any program (sub)expression as the slicing criterion. ResumenReversible CSP ComputationsGalindo, Carlos; Nishida, Naoki; Sílva, Josep; Tamarit, Salvador. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.Original publication metadata Published in: IEEE Transactions on Parallel and Distributed Systems (Volume: 32, Issue: 6, June 1 2021) Date of Publication: 14 January 2021 Pages: 1425 - 1436 (12 pages) DOI: 10.1109/TPDS.2021.3051747 Publisher: IEEE Abstract: Reversibility enables a program to be executed both forwards and backwards. This ability allows programmers to backtrack the execution to a previous state. This is essential if the computation is not deterministic because re-running the program forwards may not lead to that state of interest. Reversibility of sequential programs has been well studied and a strong theoretical basis exists. Contrarily, reversibility of concurrent programs is still very young, especially in the practical side. For instance, in the particular case of the Communicating Sequential Processes (CSP) language, reversibility is practically missing. In this article, we present a new technique, including its formal definition and its implementation, to reverse CSP computations. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. The technique proposes different forms of reversibility, including strict reversibility and causal-consistent reversibility. On the practical side, we provide an implementation of a system to reverse CSP computations that is able to highlight the source code that is being executed in each forwards/backwards computation step, and that has been optimized to be scalable to real systems.