There is growing interest in the microelectronics industry in the use of formal methods in the design, verification, and test of microelectronics systems. Our group is very well situated in this field as both software and methodology developers, and as educators.Our research gravitates around these subjects as well:
Use of a multi-paradigm specification that permits expressing object-oriented data definition and processing, orthogonal to that of synchronization and timing (HAAD), and communicating abstract state machines (ASM) for describing RT-level designs.
Verification of ASM models expressed in a subset of 1st-order logic and represented by Multiway Decision Graphs (MDG).
Use of solution methods based on the narrowing of the solution space (e.g., interval narrowing) and relational interval arithmetic as implemented in CLP (BNR) Prolog from Nortel and our own proprietary software.
For more detail about our research activites, please see projects descriptions.
The teaching personnel of the laboratory proposes graduate and under graduate courses in this field of research: