Navegación

Búsqueda

Búsqueda avanzada

El autor Jaime Sánchez-Hernández ha publicado 3 artículo(s):

1 - HR-SQL: An SQL Database System with Extended Recursion and Hypothetical Reasoning

In a former work we described the system and language R-SQL that overcomes some limitations of recursion of the relational database language SQL. Such limitations are non-linearity, mutual recursion, and some combinations of negation with recursion. In addition, R-SQL improved termination properties of recursive definitions. Next, this language was extended to include a restricted form of hypothetical relations and queries using assumptions, obtaining the language HR-SQL, and a preliminary implementation was developed for it. Here, we develop a new system HR-SQL from scratch and enhance the former system in several areas. First, hypothetical reasoning is fully integrated with recursive definitions. Second, the Python script generated by the system for computing the extension (materialization) of a database is now targeted to several state-of-the-art relational database systems. Third, the system has been interfaced to the integrated development environment ACIDE, allowing both a more friendly user interaction and a graphical view of the dependency graph that shows dependencies between relations. Fourth, being developed in Prolog, we have targeted it to both SICStus Prolog and SWI-Prolog, also providing standalone executables. Finally, the system has been extended with a bundle of commands, highly improving its capabilities with respect to the former system.

Autores: Susana Nieva / Fernando Sáenz-Pérez / Jaime Sánchez-Hernández / 
Palabras Clave:

2 - A Generic Intermediate Representation for Verification Condition Generation, Work in Progress

As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic internal representation, and how the generated conditions faithfully reflect the semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph. The paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.

Autores: Manuel Montenegro /  Ricardo Peña / Jaime Sánchez-Hernández / 
Palabras Clave: intermediate representation - program transformation. - verification conditions - verification platforms

3 - SMT-based Test-Case Generation with Complex Preconditions

We present a system which can automatically generate an exhaustive set of black-box test-cases, up to a given size, for programs under test requiring complex preconditions. The key of the approach is to translate a formal precondition into a set of constraints belonging to the decidable logics of SMT solvers. By checking the satisfiability of the constraints, then the models returned by the solver automatically synthesize the cases.We also show how to use SMT solvers to automatically check for validity the test-case results, and also to complement the black-box cases with white-box ones. Finally, we use of solver to perform what we call automatic partial verification of the program. In summary, we propose a system in which exhaustive black-box and white-box testing, result checking, and partial verification, can all be done automatically. The only extra effort required from programmers is to write formal specifications.

Autores: Ricardo Peña / Jaime Sánchez-Hernández / Miguel Garrido / Javier Sagredo / 
Palabras Clave: formal specification - SMT solvers - test-case generation - Testing