Abstract
The software validation phase takes up a significant part of the design time. In order to optimize this process, several languages offer to integrate linguistic constructs that help formal verification of safety and security properties. The talk revisited software contracts such as those used in the Spec# language, compared dynamic and static verification of software contracts, and examined more recent proposals on the verification of safety properties in Java derived from formal specifications.
