Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging

We discuss a framework for the application of abstract interpretation as an aid during program development, rather than in the more traditional application of program optimization. Program validation and detection of errors is first performed statically by comparing (partial) specifications written in terms of assertions against information obtained from (global) static analysis of the program. The results of this process are expressed in the user assertion language. Assertions (or parts of assertions) which cannot be checked statically are translated into run-time tests. The framework allows the use of assertions to be optional. It also allows using very general properties in assertions, beyond the predefined set understandable by the static analyzer and including properties defined by user programs. We also report briefly on an implementation of the framework. The resulting tool generates and checks assertions for Prolog, CLP(R), and CHIP/CLP(fd) programs, and integrates compile-time and run-time checking in a uniform way. The tool allows using properties such as types, modes, non-failure, determinacy, and computational cost, and can treat modules separately, performing incremental analysis.

Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging

We present a framework for the application of abstract interpretation as an aid during program development, rather than in the more traditional application of program optimization. Program validation and detection of errors is first performed statically by comparing (partial) specifications written in terms of assertions against information obtained from static analysis of the program. The results of this process are expressed in the user assertion language. Assertions (or parts of assertions) which cannot be verified statically are translated into run-time tests. The framework allows the use of assertions to be optional. It also allows using very general properties in assertions, beyond the predefined set understandable by the static analyzer and including properties defined by means of user programs. We also report briefly on an implementation of the framework. The resulting tool generates and checks assertions for Prolog, CLP(R), and CHIP/CLP(fd) programs, and integrates compile-time and run-time checking in a uniform way. The tool allows using properties such as types, modes, non-failure, determinacy, and computational cost, and can treat modules separately, performing incremental analysis. In practice, this modularity allows detecting statically bugs in user programs even if they do not contain any assertions.

Global optimization of solar thermophotovoltaic systems

n this paper, we present a theoretical model based on the detailed balance theory of solar thermophotovoltaic systems comprising multijunction photovoltaic cells, a sunlight concentrator and spectrally selective surfaces. The full system has been defined by means of 2n + 8 variables (being n the number of sub-cells of the multijunction cell). These variables are as follows: the sunlight concentration factor, the absorber cut-off energy, the emitter-to-absorber area ratio, the emitter cut-off energy, the band-gap energy(ies) and voltage(s) of the sub-cells, the reflectivity of the cells' back-side reflector, the emitter-to-cell and cell-to-cell view factors and the emitter-to-cell area ratio. We have used this model for carrying out a multi-variable system optimization by means of a multidimensional direct-search algorithm. This analysis allows to find the set of system variables whose combined effects results in the maximum overall system efficiency. From this analysis, we have seen that multijunction cells are excellent candidates to enhance the system efficiency and the electrical power density. Particularly, multijunction cells report great benefits for systems with a notable presence of optical losses, which are unavoidable in practical systems. Also, we have seen that the use of spectrally selective absorbers, rather than black-body absorbers, allows to achieve higher system efficiencies for both lower concentration and lower emitter-to-absorber area ratio. Finally, we have seen that sun-to-electricity conversion efficiencies above 30% and electrical power densities above 50 W/cm2 are achievable for this kind of systems.

Laser sounding from space; report of the ESA Technology Working Group on Space Laser Sounding and Ranging

The purpose and principles of spaceborne lidar are described, giving particular attention to candidates for space deployment, including simple backscatter lidar for measuring of cloud top height, cloud extend and optical properties, differential absorption lidar providing high vertical resolution measurements of humidity, temperature and pressure, a wind profiling lidar with the unique capability of improved weather forecasting and global dynamics, and a ranging and altimeter lidar for very accurate measurement of surface features, including ground, sea and ice cap height for solid earth studies.