Alpuente Frasnedo, María; Pardo Pont, Daniel; Villanueva García, Alicia
In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the K semantic framework, we enrich the symbolic execution facilities recently provided by K with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented...
This report summarises the key ideas for a simple concept of I.G. and its
explanatory value for several areas.
Alpuente Frasnedo, María; Ballis, D.; Sapiña Sanchis, Julia
In this paper, we present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification A of the program behavior that is given in the form of assertions together with an overly general program R whose execution might violate the assertions. Our technique translates R into a refined program R' in which every computation is a computation in R that satisfies the assertions of A.
Our correction technique is first formalized for topmost rewrite theories, and then we generalize it to larger rewrite theories that support nested structured...
Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José
Computing generalizers is relevant in a wide spectrum of automated
reasoning areas where analogical reasoning and inductive inference
are needed. The ACUOS system computes a complete and minimal
set of semantic generalizers (also called \anti-uni ers") of two structures
in a typed language modulo a set of equational axioms. By supporting
types and any combination of associativity (A), commutativity (C), and
unity (U) algebraic axioms for function symbols, ACUOS allows reasoning
about typed data structures, e.g. lists, trees, and (multi-)sets, and
typical hierarchical/structural relations such as is a and part of. This
paper discusses the modular ACU generalization tool ACUOS and illustrates
its use in a classical arti ficial intelligence...
COMINI, MARCO; Titolo, Laura; Villanueva García, Alicia
Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which rep- resents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and some- times the needed fragment is quite huge.
In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpreta- tion techniques)...