Hello, A PhD position on E-ACSL, the runtime annotation checker of Frama-C, is available in the Frama-C team. The team is part of Software Safety and Security Lab of CEA List, located at Paris-Saclay, France. This PhD is a collaboration between CEA List and Université d'Orléans in the context of a national project recently started. It aims at verifying multi-state properties at runtime. More details available online: https://frama-c.com/jobs/2025-01-20-multistate-rac.html Feel free to contact me for any question. Best regards, Julien Signoles Research Director | Scientific advisor CEA List, Software Safety and Security Lab | Department of Software and System Engineering Julien.Signoles@cea.fr | tel:(+33)1.69.08.00.18