The L4.verified Project and Its Next Steps
Timing Analysis of Embedded Software Systems
Embedded software is often applied in safety-criticial systems, e.g. the braking system of a car or the steering gear of an airplane. Many of these safety-critical systems are also time-critical, meaning that the calculations performed by the tasks of the embedded system need not only be functionally correct but must be carried out in a timely fashion. In this talk we show how real-time model checking using the verification tool UPPAAL (www.uppaal.com) may be used to give such timing guarantees.
Francesco Logozzo, Microsoft Research
Clousot: Language agnostic static contract checking via abstract interpretation
Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs.
CodeContracts take the form of preconditions, postconditions, and object invariants expressed as library calls. In the talk, I will introduce and demo
CodeContracts, the runtime checker, and I will describe the static
checker (Clousot), and the rationale behind its design. The CodeContracts API is part of .NET 4.0. The tools can be downloaded