In case you were wondering what CSF stands for, committee member Cédric Fournet pointed out that according to google "CSF 2014" is the 4th canine science forum ( csf2014.com ), co-located with the first feline science forum. Here in Vienna we don't have quite as many adorable puppies but we did have two exciting invited talks on Tuesday, one of which had a picture of a kitten that made the whole room laugh.
The day opened with E. Clarke reflecting on the history of model checking before announcing his retirement. That talk took a bit of effort to follow as I wasn't familiar with the various combinations of temporal quantifiers - does AG imply AF or the other way round again? - but I caught the gist of it and it's impressive just how far we've advanced in solving practical instances of what's supposed to be an undecidable problem. The idea I caught is that instead of reasoning about a particular system, you define a set of axioms that you'd hope your system to have and express them in a suitable logic, then verify properties on the level of axioms alone. Anything you can prove here must hold for any model of the axioms, so all that remains for your concrete system is to enforce the constraints of the axioms and you know a lot about what your system will or will not do.
The second invited talk on Tuesday was Acquisti's "Privacy in the age of augmented reality." This took us through a number of experiments performed to explore people's attitudes to privacy. In one experiment, students were asked questions such as whether they'd cheated in exams, which they could also decline to answer. One group was told their results would only be shared with other students, another group that lecturers may see the results as well. As expected, the second group declined to answer more often. But this was just the control - the question was, how much of a time delay do you have to insert between giving people a privacy statement (whether or not lecturers can see the results) and asking the questions, for the difference in declined answers between the two groups to disappear? The answer, it turns out, is about 15 seconds.
In another experiment, researchers set up a number of fake facebook profiles with "unique" names and sent out job applications in these names using the same template to many employers across the US. The facebook profiles between two groups in the same experiment differed in one protected characteristic, so any difference in the response rates implies that employers (1) are looking up candidates' facebook profiles (if only by searching for the name - all these profiles were public) and (2) whether consciously or not, are discriminating based on information they should never have.
The result - sexual orientation didn't make a statistically significant difference anywhere. Religion however did: while in Democrat and "mixed" states there was no significant difference, in a Republican state saying that you're Muslim on your facebook profile all but guarantees you won't even get a response to your CV. For some reason they didn't consider gender in this experiment, but one could also argue that the existence of gender discrimination in hiring is proven beyond all reasonable doubt already*.
The augmented reality part involved an experiment to see just how good face recognition and data mining have got nowadays. Based on a sample of around 100k public facebook profiles linking names to pictures, Acquisti's group constructed an app that lets you point your phone at someone and take a photo, then uploads it to the cloud and tries to find them - if successful, it displays the name as an overlay on the screen. Within about a minute, they could in some cases find not just the name but also the date of birth and most digits of the social security number - can't quite remember what the thing about the encoding of SSNs is but it's somehow linked to a public register of births and deaths. In case the app wasn't creepy enough, google glass was mentioned as the next platform they wanted to look at.
* The following, while not statistically significant on its own, is one example: http://qz.com/103453/i-understood-gender-discrimination-after-i-added-mr-to-my-resume-and-landed-a-job/