Formal specification of software systems is an old endeavor that is now yielding striking successes, in large part due to the availability of powerful new techniques for coupling specifications with running code via formal verification or automated testing. This talk surveys what’s happening in the area broadly and presents one example in more detail: a formal specification of the core behavior of a synchronization service and a specification-based random testing framework for applying it to real-world synchronizers.
