Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014-11)
The notion of *operational termination* captures nonterminating computations due to subsidiary processes that are necessary to issue a *single* `main' step but which often remain `hidden' when the main computation sequence ...
Lucas Alba, Salvador; Gutiérrez Gil, Raúl(Springer-Verlag, 2018)
[EN] In program analysis, the synthesis of models of logical theories representing the program semantics is often useful to prove program properties. We use order-sorted first- order logic as an appropriate framework to ...
Restrictions of rewriting may turn normal forms of some terms unreachable, leading to
incomplete computations. Context-sensitive rewriting (csr) is the restriction of rewriting that
only permits reductions on arguments ...
Gutiérrez Gil, Raúl; Lucas Alba, Salvador(2015-05-26)
Context-sensitive rewriting (CSR) is a variant of rewriting where only selected arguments of function symbols can be rewritten. Consequently, the subterm positions of a term are classified as either active, i.e., positions ...
Personal mobile devices like smartwatches, smartphones, tablets, etc., are just small computers with a computing performance which is similar to last-decade desktop computers. In sharp contrast, though, mobile devices ...
Innermost context-sensitive rewriting (CSR) has been proved useful for modeling the computational behavior of programs of algebraic languages like Maude. We adapt the Dependency Pairs Framework to innermost CSR since, up ...
[EN]
In Computer Science and Software Engineering, even at this time, when huge hardware and software resources are available, the problem of checking correctness of an speciﬁc piece of software is a very complicated one. ...
Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014)
Reasoning about termination of declarative programs, which are described by means of a computational logic, requires the definition of appropriate abstractions as semantic models of the logic, and also handling the conditional ...
Lucas Alba, Salvador; Meseguer, Jose(Elsevier, 2016-01)
We present several new concepts and results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs), which support types, subtypes and rewriting modulo axioms, and contains the ...
Lucas Alba, Salvador; Meseguer, José(ACM, 2014-09)
A declarative program P is a *theory* in a given computational logic L, so that *computation* with such a program is efficiently implemented as *deduction* in L. That is why *inference systems* are crucial: they both (i) ...
[EN] The semantics of computational systems (e.g., relational and knowledge data bases, query-answering systems, programming languages, etc.) can often be expressed as (the specification of) a logical theory Th. Queries, ...
Polynomial constraint solving plays a prominent role in several areas of hardware and software analysis and verification, e.g.; termination proving, program invariant generation and hybrid system verification, to name a ...
A termination problem can be transformed into a set of polynomial constraints. Up to now, several approaches have been studied to deal with these constraints as constraint solving problems. In this thesis, we study in depth ...
Lucas Alba, Salvador; Meseguer, José(Springer Verlag (Germany), 2014-11)
This paper presents several new results on conditional term rewriting within the general framework of order-sorted rewrite theories (OSRTs) which contains the more restricted framework of conditional term rewriting systems ...
[EN] Recent developments in termination analysis for declarative programs emphasize the use of appropriate models for the logical theory representing the program at stake as a generic approach to prove termination of ...
[EN] This thesis presents the implementation of a framework to work with term rewriting
systems. Term rewriting systems provide a complete computational model which is very
close to functional programming. Its formulation ...
[EN] Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for the definition of a normalization ...
Maude es un lenguaje de programación declarativo basado en la lógica de reescritura
que incorpora muchas características que lo hacen muy potente. Sin
embargo, a la hora de probar ciertas propiedades computacionales esto ...
Gutiérrez Gil, Raúl; Lucas Alba, Salvador(Sistedes, 2014-09-16)
Modularity is essential in software development, where a piece of software is often designed and implemented as a composition of simpler modules. So, if we want to prove that a program satisfies a given property, a modular ...