Sémantique formelle des opérateurs d'un langage de listes
Simulation Software Selection "Whys and Hows"
Simulation system COSMO. Description of its language and compiler
SMAL - The symbol manipulation language
Software complexity as a software quality indicator (the three doubts and the light at the end of tunnel)
Software for visualisation of small objects.
Some issues in using formal methods for the development of reactive systems.
Some key research problems in automated theorem proving for hardware and software verification.
This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In addition,...
Some new technics regarding the parallelisation of ZéBuLoN, an object oriented finite element code for structural mechanics
A finite element code, called ZéBuLoN was parallelised some years ago. This code is entirely written using an object oriented framework (C++ is the support language). The aim of this paper is to present some problems which arose during the parallelization, and some innovative solutions. Especially, a new concept of message passing is presented which allows to take into account SMP machines while still using the parallel virtual machine abstraction.
Some new technics regarding the parallelisation of ZéBuLoN, an object oriented finite element code for structural mechanics
A finite element code, called ZéBuLoN was parallelised some years ago. This code is entirely written using an object oriented framework (C++ is the support language). The aim of this paper is to present some problems which arose during the parallelization, and some innovative solutions. Especially, a new concept of message passing is presented which allows to take into account SMP machines while still using the parallel virtual machine abstraction.
Some Notes on the Formal Definition of Streams
State spaces and dipaths up to dihomotopy.
Stochastic differential equation-based flexible software reliability growth model.
Sur l'élimination itérative des situations de blocage dans un système
Symbolic Implementation of the Hooke-Jeeves Method
Synchronous parallelizations of serial computer programs
Syntactical definitions of program and flow diagram
Taclets: a new paradigm for constructing interactive theorem provers.
Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules...
Teoria dei domini nell’interpretazione astratta: equazioni, completezza e logica
Termination checking with types
The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is...