تجزیه و تحلیل استاتیک از نرم افزار همزمان یکپارچه شده با اولویت های پویا

We illustrate our construction formally on an idealized language. Following previous work, we first provide a concrete semantics in thread-modular denotational form that is complete for safety properties, and then show how to apply classic abstractions to obtain an effective static analyzer, able to detect all run-time errors, data-races, as well as deadlocks. Finally, we briefly discuss our implementation inside the Astrée analyzer and on-going experimentation, with results limited for now to small programs.