Supporting pruning in tabled LP

This paper analyzes issues which appear when supporting pruning operators in tabled LP. A version of the once/1 control predicate tailored for tabled predicates is presented, and an implementation analyzed and evaluated. Using once/1 with answer-on-demand strategies makes it possible to avoid computing unneeded solutions for problems which can benefit from tabled LP but in which only a single solution is needed, such as model checking and planning. The proposed version of once/1 is also directly applicable to the efficient implementation of other optimizations, such as early completion, cut-fail loops (to, e.g., prune at the top level), if-then-else, and constraint-based branch-and-bound optimization. Although once/1 still presents open issues such as dependencies of tabled solutions on program history, our experimental evaluation confirms that it provides an arbitrarily large efficiency improvement in several application areas.

Abstraction-carrying code: a model for mobile code safety

Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The intended benefit is that the program consumer can locally validate the certificate w.r.t. the "untrustcd" program by means of a certificate checker a process which should be much simpler, efficient, and automatic than generating the original proof. The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both proving programs correct and replacing a costly verification process by an efficient checking proceduri on th( consumer side. In this work we propose Abstraction- Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safely policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certificate. The validity of the abstraction on ihe consumer side is checked in a single pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the area of mobile code safety.

Context-sensitive multivariant assertion checking in modular programs

We propose a modular, assertion-based system for verification and debugging of large logic programs, together with several interesting models for checking assertions statically in modular programs, each with different characteristics and representing different trade-offs. Our proposal is a modular and multivariant extensión of our previously proposed abstract assertion checking model and we also report on its implementation in the CiaoPP system. In our approach, the specification of the program, given by a set of assertions, may be partial, instead of the complete specification required by raditional verification systems. Also, the system can deal with properties which cannot always be determined at compile-time. As a result, the proposed system needs to work with safe approximations: all assertions proved correct are guaranteed to be valid and all errors actual errors. The use of modular, context-sensitive static analyzers also allows us to introduce a new distinction between assertions checked in a particular context or checked in general.

Checking existing formulas for estimating overtopping rates in harbour breakwaters

The purpose of the research work resulting from various studies undertaken in the CEDEX, as summarized in this article, is to make a comparative analysis of methods for calculating overtopping rates developed by different authors. To this effect, in the first place, existing formulas for estimating the overtopping rate on rubble mound and vertical breakwaters were summarised and analysed. Later, the above mentioned formulas were compared using the results obtained in a series of hydraulic model tests at the CEDEX. The results obtained in the Ferrol outer harbour breakwater and Melilla harbour breakwater tests are presented here. A calculation method based on the neural network theory, developed in the European CLASH Project, was applied to a series of sloping breakwater tests in order to complete this research and the results obtained in the Ferrol outer harbour breakwater test are presented in this article. A series of additional tests was also carried out in a physical model on the standard cross section of the Bilbao harbour sloping breakwater’s cross section, the results of which are under study using the empirical formulas applicable to the cross section, as well as the NN-OVERTOPPING neural network