Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code

This collection of papers focuses on improving software safety and verification across domains likely to impact security posture: embedded automotive C (a Frama‑C plugin and a C module interface contract language to check control/data‑flow and restrict calls from untrusted modules); governance of runtime code materialization (reclassifying eval as a governed effect to inspect capability/policy before execution); automated generation of code‑security benchmarks and exploits (AutoBaxBuilder/AutoBaxBench) to scale evaluation of LLM‑generated code; a preliminary empirical comparison showing Move (