Abstract Interpretation-based verification/certification in the ciaoPP system

CiaoPP is the abstract interpretation-based preprocessor of the Ciao multi-paradigm (Constraint) Logic Programming system. It uses modular, incremental abstract interpretation as a fundamental tool to obtain information about programs. In CiaoPP, the semantic approximations thus produced have been applied to perform high- and low-level optimizations during program compilation, including transformations such as múltiple abstract specialization, parallelization, partial evaluation, resource usage control, and program verification. More recently, novel and promising applications of such semantic approximations are being applied in the more general context of program development such as program verification. In this work, we describe our extensión of the system to incorpórate Abstraction-Carrying Code (ACC), a novel approach to mobile code safety. ACC follows the standard strategy of associating safety certificates to programs, originally proposed in Proof Carrying- Code. A distinguishing feature of ACC is that we use an abstraction (or abstract model) of the program computed by standard static analyzers as a certifícate. The validity of the abstraction on the consumer side is checked in a single-pass by a very efficient and specialized abstractinterpreter. We have implemented and benchmarked ACC within CiaoPP. The experimental results show that the checking phase is indeed faster than the proof generation phase, and that the sizes of certificates are reasonable. Moreover, the preprocessor is based on compile-time (and run-time) tools for the certification of CLP programs with resource consumption assurances.

Some techniques for automated, resource-aware distributed and mobile computing in a multi-paradigm programming system

Distributed parallel execution systems speed up applications by splitting tasks into processes whose execution is assigned to different receiving nodes in a high-bandwidth network. On the distributing side, a fundamental problem is grouping and scheduling such tasks such that each one involves sufñcient computational cost when compared to the task creation and communication costs and other such practical overheads. On the receiving side, an important issue is to have some assurance of the correctness and characteristics of the code received and also of the kind of load the particular task is going to pose, which can be specified by means of certificates. In this paper we present in a tutorial way a number of general solutions to these problems, and illustrate them through their implementation in the Ciao multi-paradigm language and program development environment. This system includes facilities for parallel and distributed execution, an assertion language for specifying complex programs properties (including safety and resource-related properties), and compile-time and run-time tools for performing automated parallelization and resource control, as well as certification of programs with resource consumption assurances and efñcient checking of such certificates.

Programming with global analysis

Global data-flow analysis of (constraint) logic programs, which is generally based on abstract interpretation [7], is reaching a comparatively high level of maturity. A natural question is whether it is time for its routine incorporation in standard compilers, something which, beyond a few experimental systems, has not happened to date. Such incorporation arguably makes good sense only if: • the range of applications of global analysis is large enough to justify the additional complication in the compiler, and • global analysis technology can deal with all the features of "practical" languages (e.g., the ISO-Prolog built-ins) and "scales up" for large programs. We present a tutorial overview of a number of concepts and techniques directly related to the issues above, with special emphasis on the first one. In particular, we concéntrate on novel uses of global analysis during program development and debugging, rather than on the more traditional application área of program optimization. The idea of using abstract interpretation for validation and diagnosis has been studied in the context of imperative programming [2] and also of logic programming. The latter work includes issues such as using approximations to reduce the burden posed on programmers by declarative debuggers [6, 3] and automatically generating and checking assertions [4, 5] (which includes the more traditional type checking of strongly typed languages, such as Gódel or Mercury [1, 8, 9]) We also review some solutions for scalability including modular analysis, incremental analysis, and widening. Finally, we discuss solutions for dealing with meta-predicates, side-effects, delay declarations, constraints, dynamic predicates, and other such features which may appear in practical languages. In the discussion we will draw both from the literature and from our experience and that of others in the development and use of the CIAO system analyzer. In order to emphasize the practical aspects of the solutions discussed, the presentation of several concepts will be illustrated by examples run on the CIAO system, which makes extensive use of global analysis and assertions.

A generic framework for context-sensitive analysis of modular programs

Context-sensitive analysis provides information which is potentially more accurate than that provided by context-free analysis. Such information can then be applied in order to validate/debug the program and/or to specialize the program obtaining important improvements. Unfortunately, context-sensitive analysis of modular programs poses important theoretical and practical problems. One solution, used in several proposals, is to resort to context-free analysis. Other proposals do address context-sensitive analysis, but are only applicable when the description domain used satisfies rather restrictive properties. In this paper, we argüe that a general framework for context-sensitive analysis of modular programs, Le., one that allows using all the domains which have proved useful in practice in the non-modular setting, is indeed feasible and very useful. Driven by our experience in the design and implementation of analysis and specialization techniques in the context of CiaoPP, the Ciao system preprocessor, in this paper we discuss a number of design goals for context-sensitive analysis of modular programs as well as the problems which arise in trying to meet these goals. We also provide a high-level description of a framework for analysis of modular programs which does substantially meet these objectives. This framework is generic in that it can be instantiated in different ways in order to adapt to different contexts. Finally, the behavior of the different instantiations w.r.t. the design goals that motivate our work is also discussed.

An assertion language for constraint logic programs

In an advanced program development environment, such as that discussed in the introduction of this book, several tools may coexist which handle both the program and information on the program in different ways. Also, these tools may interact among themselves and with the user. Thus, the different tools and the user need some way to communicate. It is our design principie that such communication be performed in terms of assertions. Assertions are syntactic objects which allow expressing properties of programs. Several assertion languages have been used in the past in different contexts, mainly related to program debugging. In this chapter we propose a general language of assertions which is used in different tools for validation and debugging of constraint logic programs in the context of the DiSCiPl project. The assertion language proposed is parametric w.r.t. the particular constraint domain and properties of interest being used in each different tool. The language proposed is quite general in that it poses few restrictions on the kind of properties which may be expressed. We believe the assertion language we propose is of practical relevance and appropriate for the different uses required in the tools considered.

Some issues in analysis and specialization of modular ciao-prolog programs

Separating programs into modules is a well-known technique which has proven very useful in program development and maintenance. Starting by introducing a number of possible scenarios, in this paper we study different issues which appear when developing analysis and specialization techniques for modular logic programming. We discuss a number of design alternatives and their consequences for the different scenarios considered and describe where applicable the decisions made in the Ciao system analyzer and specializer. In our discussion we use the module system of Ciao Prolog. This is both for concreteness and because Ciao Prolog is a second-generation Prolog system which has been designed with global analysis and specialization in mind, and which has a strict module system. The aim of this work is not to provide a theoretical basis on modular analysis and specialization, but rather to discuss some interesting practical issues.

A new module system for prolog

It is now widely accepted that separating programs into modules has proven very useful in program development and maintenance. While many Prolog implementations include useful module systems, we feel that these systems can be improved in a number of ways, such as, for example, being more amenable to effective global analysis and allowing sepárate compilation or sensible creation of standalone executables. We discuss a number of issues related to the design of such an improved module system for Prolog. Based on this, we present the choices made in the Ciao module system, which has been designed to meet a number of objectives: allowing sepárate compilation, extensibility in features and in syntax, amenability to modular global analysis, etc.

An overview of ciao and its design philosophy

We provide an overall description of the Ciao multiparadigm programming system emphasizing some of the novel aspects and motivations behind its design and implementation. An important aspect of Ciao is that, in addition to supporting logic programming (and, in particular, Prolog), it provides the programmer with a large number of useful features from different programming paradigms and styles and that the use of each of these features (including those of Prolog) can be turned on and off at will for each program module. Thus, a given module may be using, e.g., higher order functions and constraints, while another module may be using assignment, predicates, Prolog meta-programming, and concurrency. Furthermore, the language is designed to be extensible in a simple and modular way. Another important aspect of Ciao is its programming environment, which provides a powerful preprocessor (with an associated assertion language) capable of statically finding non-trivial bugs, verifying that programs comply with specifications, and performing many types of optimizations (including automatic parallelization). Such optimizations produce code that is highly competitive with other dynamic languages or, with the (experimental) optimizing compiler, even that of static languages, all while retaining the flexibility and interactive development of a dynamic language. This compilation architecture supports modularity and separate compilation throughout. The environment also includes a powerful autodocumenter and a unit testing framework, both closely integrated with the assertion system. The paper provides an informal overview of the language and program development environment. It aims at illustrating the design philosophy rather than at being exhaustive, which would be impossible in a single journal paper, pointing instead to previous Ciao literature.

The ciao prolog system

Ciao is a public domain, next generation multi-paradigm programming environment with a unique set of features: Ciao offers a complete Prolog system, supporting ISO-Prolog, but its novel modular design allows both restricting and extending the language. As a result, it allows working with fully declarative subsets of Prolog and also to extend these subsets (or ISO-Prolog) both syntactically and semantically. Most importantly, these restrictions and extensions can be activated separately on each program module so that several extensions can coexist in the same application for different modules. Ciao also supports (through such extensions) programming with functions, higher-order (with predicate abstractions), constraints, and objects, as well as feature terms (records), persistence, several control rules (breadth-first search, iterative deepening, ...), concurrency (threads/engines), a good base for distributed execution (agents), and parallel execution. Libraries also support WWW programming, sockets, external interfaces (C, Java, TclTk, relational databases, etc.), etc. Ciao offers support for programming in the large with a robust module/object system, module-based separate/incremental compilation (automatically -no need for makefiles), an assertion language for declaring (optional) program properties (including types and modes, but also determinacy, non-failure, cost, etc.), automatic static inference and static/dynamic checking of such assertions, etc. Ciao also offers support for programming in the small producing small executables (including only those builtins used by the program) and support for writing scripts in Prolog. The Ciao programming environment includes a classical top-level and a rich emacs interface with an embeddable source-level debugger and a number of execution visualization tools. The Ciao compiler (which can be run outside the top level shell) generates several forms of architecture-independent and stand-alone executables, which run with speed, efficiency and executable size which are very competive with other commercial and academic Prolog/CLP systems. Library modules can be compiled into compact bytecode or C source files, and linked statically, dynamically, or autoloaded. The novel modular design of Ciao enables, in addition to modular program development, effective global program analysis and static debugging and optimization via source to source program transformation. These tasks are performed by the Ciao preprocessor ( ciaopp, distributed separately). The Ciao programming environment also includes lpdoc, an automatic documentation generator for LP/CLP programs. It processes Prolog files adorned with (Ciao) assertions and machine-readable comments and generates manuals in many formats including postscript, pdf, texinfo, info, HTML, man, etc. , as well as on-line help, ascii README files, entries for indices of manuals (info, WWW, ...), and maintains WWW distribution sites.

Reversible language extensions and their application in debugging

A range of methodologies and techniques are available to guide the design and implementation of language extensions and domainspecific languages. A simple yet powerful technique is based on source-tosource transformations interleaved across the compilation passes of a base language. Despite being a successful approach, it has the main drawback that the input source code is lost in the process. When considering the whole workflow of program development (warning and error reporting, debugging, or even program analysis), program translations are no more powerful than a glorified macro language. In this paper, we propose an augmented approach to language extensions for Prolog, where symbolic annotations are included in the target program. These annotations allow selectively reversing the translated code. We illustrate the approach by showing that coupling it with minimal extensions to a generic Prolog debugger allows us to provide users with a familiar, source-level view during the debugging of programs which use a variety of language extensions, such as functional notation, DCGs, or CLP{Q,R}.

Fiabilidad de minimodulos de silicio

El objetivo de este Proyecto Final de Carrera es la realización de un ensayo de fiabilidad de componentes electrónicos, más concretamente de Minimódulos de Silicio, con el fin de estudiar su comportamiento a lo largo del tiempo de vida. Debido a la larga duración de los Minimódulos de Silicio , un ensayo de este tipo podría durar años, por lo que es necesario realizar un ensayo acelerado que acorte significativamente el tiempo del experimento, para ello, han de someterse a esfuerzos mayores que en condiciones normales de funcionamiento. A día de hoy, los Minimódulos de silicio, que conocemos como placas solares fotovoltaicas, se usan en infinidad de dispositivos debido a las múltiples ventajas que conllevan. La principal ventaja es poder llevar electricidad a cualquier parte del planeta sin necesidad de tener que hacer unas elevadas inversiones. Esta electricidad proviene de una fuente de energía inagotable y nada contaminante, con lo que ayudamos a mantener el equilibrio del planeta. La mayoría de las veces estas placas solares fotovoltaicas se usan en el exterior, soportando cambios de temperatura y de humedad elevados, de ahí, la importancia de realizar ensayos de fiabilidad, que muestren sus posibles causas de fallo, los efectos que producen estos fallos y los aspectos de diseño, fabricación y mantenimiento que puedan afectarles. Los Minimódulos de silicio utilizados en este proyecto son el modelo MC-SP0.8-NF-GCS de la empresa fabricante Multicomp. Para realizar el Proyecto hubiéramos necesitado una cámara climática que simulara unas condiciones ambientales determinadas, pero debido a la dificultad de iluminar el módulo dentro de la cámara climática hemos desarrollado un nuevo sistema de ensayos acelerados en temperatura. El nuevo sistema de ensayos acelerados consiste en: •Colocar los módulos fotovoltaicos en el laboratorio con un foco de 500W que irradia lo equivalente al sol. •Los tres módulos trabajarán a tres temperaturas diferentes para simular condiciones ambientales distintas, concretamente a 60°C, 72°C y 84°C. •Mediante un sistema automático de medida diseñado en LabVIEW, de manera simultánea tomará medidas de tensión en las tres placas y estudiaremos el grado degradación en cada placa. Se analizaran los resultados obtenido de cada una de las medidas y se realizará un estudio de fiabilidad y del proceso de degradación sufrido por los Minimódulos de silicio. Este PFC se puede dividir en las siguientes fases de trabajo siendo el ensayo la parte más larga en el tiempo: •Búsqueda de bibliografía documentación y normas aplicables. •Familiarización con los equipos y software, estudiando el manejo del software que viene con el Multímetro Keithley 2601 y el programa LabVIEW. •Desarrollo del hardware y sistemas necesarios para la realización del ensayo. •Montaje del ensayo •Realización del ensayo. •Análisis de resultados. ABSTRACT. The objective of this Final Project is conducting a test reliability of electronic components, more specifically Silicon minimodules, in order to study their behavior throughout the life span. Due to the long duration of Silicon minimodules a test like this could take years, so it is necessary to perform an accelerated significantly shorten the time of the experiment, testing for it, should be subjected to greater efforts than in normal operating. Today, the mini-modules, silicon is known as photovoltaic solar panels are used in a multitude of devices due to the many advantages they bring. The main advantage is to bring electricity to anywhere in the world without having to make high investments. This electricity comes from an inexhaustible source of energy and no pollution, thus helping to maintain the balance of the planet. Most of the time these solar photovoltaic panels are used on the outside, enduring changes in temperature and high humidity, hence, the importance of reliability testing, showing the possible causes of failure, the effects produced by these faults and aspects of design, manufacturing and maintenance that may affect them. The silicon mini-modules used in this project are the MC-SP0.8-NF-GCS model Multicomp manufacturing company. To realize the project we would have needed a climatic chamber to simulate specific environmental conditions, but due to the difficulty of illuminating the module in the climate chamber we have developed a new system of accelerated tests in temperature. The new system is accelerated tests: •Place the PV modules in the laboratory with a focus on the equivalent 500W radiating sun. •The three modules work at three different temperatures to simulate different environmental conditions, namely at 60 °C, 72 °C and 84 °C. •Automatic measurement system designed in LabVIEW, simultaneous voltage measurements taken at the three plates and study the degradation degree in each plate. The results obtained from each of the measurements and a feasibility study and degradation suffered by the silicon is performed minimodules were analyzed. This PFC can be divided into the following phases of the test work the longest part being overtime: •Literature search and documentation standards. •Familiarization with equipment and software, studying management software that comes with the Keithley 2601 multimeter and the LabVIEW program. •Development of hardware and systems necessary for the conduct of the trial. •Experiment setup •Carrying out the experiment. •Analysis of results.

Resilience through Adversity: A narrative case study of students' experiences of expulsion from school

Expulsion from school is life changing. This single event can alter the trajectory of a student's life--for better or for worse. How life changes is unique for each individual student. Risk and protective factors that impact an individual student's resilience determine the level of positive or negative outcomes experienced as a result of expulsion. Educators have the opportunity to take advantage of this disruption in students' education to improve the trajectory of students' lives. However, without thoughtful intervention from caring educators, this interruption in students' education may have an irreparable destructive impact on students' future. The purpose of this study was to understand the expulsion experience from the point of view of the student in order to represent this critical stakeholder group in future policy and program development, implementation, and decision-making. Students' narratives are a means for members of the educational community to access students' experiences and perceptions in order to understand the impact of expulsion on students' lives. Students' perspectives are presented through thick description in this narrative case study. The experience of these eight students is evidence that expulsion can change students' lives in a positive way. Knowing this, responsible educators must develop interventions for expelled students that channel the positive life-changing potential of this experience. Educators must develop interventions focused on bringing forth protective factors that are documented to increase resilience and to make students less susceptible to the risks inherent in removing them from school. Recommendations for educators and policy-makers are presented to assist educators in preventing expulsion and improving educational and socio-emotional outcomes for expelled students.

Community health representative; a changing philosophy of Indian involvment.

Mode of access: Internet.

Motor vehicle occupant safety survey. Final report.

National Highway Traffic Safety Administration, Office of Program Development and Evaluation, Washington, D.C.

Summary statistics of the national railroad-highway crossing inventory for public at-grade crossings. Final report.

Federal Railroad Administration, Office of Policy and Program Development, Washington, D.C.