Ait Mohamed, Otmane

With recent advances in silicon foundries, which continue to aggressively reduce the physical dimensions of silicon structures, and advances in design technologies, which enable engineers to build larger and more complex designs, proving the correctness of these systems becomes the greatest challenge. In this research program, we are interested in developing techniques and tools to enhance the usefulness of formal verification for the analysis and verification of large-scale systems. For example, we are interested in the link between the simulation-based approach and the model-checking approach. By adding a set of assertions to the design that define the desired behavior of each block of the design, we can synthesize monitors to verify the validity of the design on the one hand, and derive constraints on the other. These constraints can be used with a model checker.