Search

This paper presents the implementation of a program transformation that removes square roots and divisions from functional programs without recursion, producing code that can be exactly computed. This transformation accepts different subsets of languages as input and it provides a certifying mechanism when the targeted language is Pvs. In this case, we provide a relation between every function definition in the output code and its corresponding one in the input code, that specifies the behavior of the produced function with respect to the input one. This transformation has been implemented in OCaml and has been tested on different algorithms from the NASA ACCoRD project.

In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs -- such as record field access -- for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records.

We propose a formalization of generic algorithms that includes analog algorithms. This is achieved by reformulating and extending the framework of abstract state machines to include continuous-time models of computation. We prove that every hybrid algorithm satisfying some reasonable postulates may be expressed precisely by a program in a simple and expressive language.

The realization of a language design requires multiple artifacts that redundantly encode the same information. This entails significant effort for language implementors, and often results in late detection of errors in language definitions. In this paper we present a proof-of-concept language designer's workbench that supports generation of IDEs, interpreters, and verification infrastructure from a single source. This constitutes a first milestone on the way to a system that fully automates language implementation and verification.

International audience; In this paper we present a new strategy for PVS that imple- ments a square root and division elimination in order to use automatic arithmetic strategies that were not able to deal with these operations in the ﰁrst place. This strategy relies on a PVS formalization of the square root and division elimination and deep embedding of PVS expressions inside PVS. Therefore using computational reﰂection and symbolic com- putation we are able to automatically transform expressions into division and square root free ones before using these decision procedures.

The use of real numbers in a program can introduce differences between the expected and the actual behavior of the program, due to the finite representation of these numbers. Therefore, one may want to define programs using real numbers such that this difference vanishes. This paper defines a program transformation for a certain class of programs that improves the accuracy of the computations on real number representations by removing the square root and division operations from the original program in order to enable exact computation with addition, multiplication and subtraction. This transformation is meant to be used on embedded systems, therefore the produced programs have to respect constraints relative to this kind of code. In order to ensure that the transformation is correct, i.e., preserves the semantics, we also aim at specifying and proving this transformation using the PVS proof assistant.

Part 1: Smart Cards System Security; International audience; Smart card Web server provides a modern interface between smart cards and the external world. It is of paramount importance that this new software component does not jeopardize the security of the smart card. This paper presents a formal model of the smart card Web server specification and the proof of its security properties. The formalization enables a thoughtful analysis of the specification that has revealed several ambiguities and potentially dangerous behaviors. Our formal model is built using a modular approach upon a model of Java Card and Global Platform. By proving the security properties, we show that the smart card Web server preserves the security policy of the overall model. In other words, this component introduces no illegal access to the card resources (i.e., file system and applications). Furthermore, the smart card Web server provides a means for securely managing the card contents (i.e., resources update).

二宮文庫 | https://www.tulips.tsukuba.ac.jp/lib/ja/collection/bunko-collection#238, A Paris : Chez Theodore Girard, dans la Grand' Salle du Palais, du costé de la Cour des Aydes, à l'Enuie , 1666, [24], 1096 [i.e. 1084], [24] p. ; 39 cm. (Fol.), Divisées en trois livres. Corrigées & augmentées de plusieurs edicts, ordonnances, arrests, & reglemens, par M.F.P.A. Et en cette derniere edition, du traité de la iurisdiction de la connestablie & mareschaussée de France, à la Table de Marbre du Palais à Paris.Errors in paging: p. 72-77, 431-436 [i.e. 425-430] are omitted; p. 110 [i.e. 104], 389 [i.e. 383], 551-554 [i.e. 539-542], 570 [i.e. 558], 873 [i.e. 861], 968 [i.e. 956], 969 [i.e. 957], 976 [i.e. 964] numbered 118, 839, 561-564, 70, 843, 668, 966, 676Signatures: [dagger][2] ã[2] ẽ[2] ĩ[2] õ[2] ũ[2] A-6V[4] 6X[2] 6Y-7A[4] (2O1 misprinted O1)