Difference between heartwood and sapwood
Forest Products Laboratory (U.S.)
1919
Search results
19 records were found.
As a specification carries out relevant information concerning the behaviour of a program, why not explore this fact to slice a program in a semantic sense aiming at optimizing it or easing its verification? It was this idea that Comuzzi, in 1996, introduced with the notion of postcondition-based slicing | slice a program using the information contained in the postcondition (the condition Q that is guaranteed to hold at the exit of a program). After him, several advances were made and different extensions were proposed, bridging the two areas of Program Verification and Program Slicing: specifically precondition-based slicing and specification-based slicing. The work reported in this Ph.D. dissertation explores further relations between these two areas aiming at discovering mutual benefits.
A deep study of specification-based slicing h...
Completely convinced of the benefits of Perl for the implementation of language processors and after doing a deep review of the state of the art on parser generation in Perl, we have identified a clear need for a powerful tool that accepts attribute grammars and builds compilers in Perl. The ob jective of this paper is to present a solution based on the developing of a back-end for ANTLR to generate attribute based language processors in Perl, to overcome the lack of this kind tools described in the preliminary study referred above. To achieve the intended ob jective, the parser generator tool ANTLR was studied in detail to understand its components and to plan the best strategies to perform the necessary retargeting of its back-end. In this process, the Java compilers generated by ANTLR were analysed carefully to learn the algorithms ad...
In the last years, the concern with the correctness of programs has been leading programmers to enrich their programs with annotations following the principles of design-by-contract, in order to be able to guarantee their correct behaviour and to facilitate reuse of verified components without having to reconstruct proofs of correctness.
In this paper we adapt the idea of specification-based slicing to the scope of (contract-based) program verification systems and behaviour specification languages. In this direction, we introduce the notion of contract-based slice of a program and show how any specification-based slicing algorithm can be used as the basis for a contract-based slicing algorithm.
These are the proceedings for the eighth national conference on XML, its Associated Technologies and its Applications (XATA'2010).
The paper selection resulted in 33% of papers accepted as full papers, and 33% of papers accepted as short papers. While these two types of papers were distinguish during the conference, and they had different talk duration, they all had the same limit of 12 pages.
We are happy that the selected papers focus both aspects of the conference: XML technologies, and XML applications.
In the first group we can include the articles on parsing and transformation technologies, like “Processing XML: a rewriting system approach", “Visual Programming of XSLT from examples", “A Refactoring Model for XML Documents", “A Performance based Approach for Processing Large XML Files in Multicore Machines", “XML to paper publ...
To prove the correctness of a program (written in a high level programming language) with respect to a specification (a set of proof obligations) does not assure the correctness of the machine code
that the end-user will run after compilation and deployment phases. The code generated by the compiler should be verified again to guarantee
that its correctness was preserved, and then that it can be executed in safety.
In the context of a Ph.D. work in the area of software analysis and transformation, we are looking for a suitable approach to prove that the
software properties (validated at source level) are kept during translation.
In this position paper we introduce our architectural proposal, and discuss the platform and we are building for Java+JML on the top of Eclipse.
In this poster we describe a work in progress
aimed at using a variant of specification-based slicing to
improve the reuse of annotated software components, developed
under the so called design-by-contract approach. We have
named this variant as contract-based because we use the
annotations, more precisely the pre and post-conditions, to slice
programs intra and inter-procedures. The idea, expressed in
the poster, is to take the pre-condition of the reused annotated
component as slicing criterion, and slice backward the program
where the component is called. In that way, we can isolate the
statements that have influence on the variables involved on the
pre-condition and check if it is preserved by that invocation,
or not.
In this paper we present the GamaSlicer tool, which is primarily a
semantics-based program slicer that also offers formal verification
(generation of verification conditions) and program visualization
functionality. The tool allows users to obtain slices using a
number of different families of slicing algorithms (\precond-based,
\postcond-based, and specification-based), from a correct software
component annotated with pre and postconditions (contracts written
in JML-annotated Java). Each family in turn contains algorithms of
different precision (with more precise algorithms being
asymptotically slower). A novelty of our work at the theoretical
level is the inclusion of a new, much more effective algorithm for
specification-based slicing, and in fact other current work at this
level is being progressively inco...
There are some modules on Comprehensive Perl Archive Network to help with the parser generation process in Perl. Unfortunately, some are limited, only supporting a particular parser algorithm and do not covering some developer needs. In this document we will analyse some of these modules, testing them in terms of performance and usability, allowing a proper evaluation of the results and careful considerations about the state of art of parser generation using Perl.
The integration of Software components within complex industrial applications with severe security standards, requires strict quality assessment of each integrated component. That is, requires a guarantee that each component is compliant with the software development good practices and all the standards in use. If full certification is easy to obtain for proprietary modules, it is particularly hard to achieve when dealing with Open-Source Software pieces, demanding for rigorous methods and techniques to implement their certification process.
In this context, code analysis plays an important role as the basis for the automatization of quality assessment of open source software projects – code analysis provides the techniques and tools to implement the necessary validation process. Although source code is still the most explored (the mai...
The European Space Agency (ESA) uses an engine to perform tests in the Ground Segment infrastructure, specially the Operational Simulator. This engine uses many different tools to ensure the development of regression testing infrastructure and these tests perform black-box testing to the C++ simulator implementation.
VST (VisionSpace Technologies) is one of the companies that provides these services to ESA and they need a tool to infer automatically tests from the existing C++ code, instead of writing manually scripts to perform tests.
With this motivation in mind, this paper explores automatic testing approaches and tools in order to propose a system that satisfies VST needs.
