Jácome Cunha

Spreadsheets are being used with many different purposes that range from toy applications to complete information systems. In any of these cases, they are often used as data repositories that can grow significantly. As the amount of data grows, it also becomes more difficult to extract concrete information out of them.
This paper focuses on the problem of spreadsheet querying. In particular, we propose an expressive and composable technique where intuitive queries can be defined. Our approach builds on a model-driven spreadsheet development environment, and queries are expressed referencing entities in the model of a spreadsheet instead of in its actual data. Finally, the system that we have implemented relies on Google’s query function for spreadsheets.

This paper presents a framework for the analysis of software artifacts. We revise and propose techniques that aid in the manipulation and combination of target-language specific tools, and in handling and controlling the results of such tools. We also propose to integrate under our framework techniques that are capable of performing language independent analyses.
The final result of our work is an analysis environment that is modular and flexible and that allows easy and elegant implementations of complex analysis suites.
We finally conduct a proof of concept for our framework by analyzing a well-known, widely used open-source software package.

Attribute grammars are a suitable formalism to express complex software language analysis and manipulation algorithms, which rely on multiple traversals of the underlying syntax tree. Recently, Attribute Grammars have been extended with mechanisms such as references and high-order and circular attributes. Such extensions provide a powerful modular mechanism and allow the specification of complex fix-point computations. This paper defines an elegant and simple, zipper-based embedding of attribute grammars and their extensions as first class citizens. In this setting, language specifications are defined as a set of independent, off-the-shelf components that can easily be composed into a powerful, executable language processor. Several real examples of language specification and processing programs have been implemented in this setting.

A central issue in program verification is the generation of verification conditions (VCs): proof obligations which, if successfully discharged, guarantee the correctness of a program vis-a`-vis a given specification. While the basic theory of program verification has been around since the 1960s, the late 1990s saw the advent of practical tools for the verification of realistic programs, and research in this area has been very active since then. Automated theorem provers have contributed decisively to these developments.
This paper establishes a basis for the generation of verifi- cation conditions combining forward and backward reasoning, for programs consisting of mutually-recursive procedures an- notated with contracts and loop invariants. We introduce also a visual technique to verify a program, in an interactive way, using Verification Graphs (VG), where a VG is a Control Flow Graph (CFG) whose edges are labeled with contracts (pre- and postconditions). This technique intends to help a software engineer to find statements that are not valid with respect to the program’s specification.

n the context of software dependability, the software verification process has an important role. Formal verification of programs is an activity that can be inserted in this process to improve software reliability. This paper presents the definition of an approach that employs a formal verification technique based on abstract interpretation. The main goal is to apply this technique as a formal activity in the software verification process to help software engineers identify programs faults. The applicability of the proposed approach is demonstrated by a case study based on embedded aerospace control software. The results obtained from its use show that abstract interpretation can contribute to software dependability.

The standard SPARK deductive verification tools, based on contracts, are not practical in early stages when the idea is only bug catching. We discuss the implementation of a bounded model checker for SPARK, focusing on specific challenges of this language. Our tool is fully automatic, complementing the existing tools for SPARK.