Sémantique des processus communicants
Sémantique logique et dénotationnelle des interpréteurs PROLOG
Some geometric perspectives in concurrency theory.
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,...
Systèmes de déduction pour les arbres et les schémas de programmes (I)
Systèmes de déduction pour les arbres et les schémas de programme (II)