Location: CLT701 Date/Time: 2nd September 2014, 14:00 - 15:00
Speaker(s): Mike Dodds.
Brief Description:In this talk, I will describe Concurrent Abstract Predicates (CAP) a variant of separation logic aimed at guaranteeing that such algorithms behave correctly. I will show how this approach can capture straightforward programmer intuitions such as data locality, resource sharing, and thread protocols. I will also explore some of the theory underlying CAP, and discuss its applications to real-world systems.
Location: CLT701 Date/Time: 9th September 2014, 14:00 - 16:00
Speaker(s): Dr. Paolo Masci.
Brief Description:In this talk, we illustrate our work carried out in collaboration with the FDA for the analysis of user interface software using formal methods technologies. A concrete example is presented that involved the analysis of user software source code from a marketed device. The source code is formally analysed within the Prototype Verification System (PVS), a state-of-the-art formal methods technology developed at SRI International. First, the source code of the device is transformed into an executable PVS model. Then, the PVS model is verified against relevant safety and usability requirements using the PVS theorem prover. During the analysis, realistic prototypes of the device are automatically generated using the PVSio-web prototyping environment with the aim to assess the relevance of identified design issues/flaws.