Resilience & Sustainability

Getting software right with properties, generated tests, and proofs

Evolve your hack into robust software!
Dijkstra
Mike Sperber
How do we write software that works - or rather, how do we ensure it's correct once it's written? We can just try it out and run it, and see if it works on a few examples. If the program was correct to begin with, that's great - but if it's not, we're going to miss bugs. Bugs that might crash our computer, make it vulnerable to attacks, stop the factory, endanger lives, or "just" leave us unsatisfied. This talk is about techniques every programmer can use to avoid large classes of bugs. You think about general properties of the things in your code, verify them through automatically generated tests, and (when it's particularly critical) proofs. This is a surprisingly fun and satisfying experience, and any programmer can do it. You need just a bit of high school math (which we'll refresh in the talk) to get started.
This talk is specifically about accessible techniques: Almost any program, function, or entity has a few interesting properties, and teasing them out will enhance your understanding of what is going on in your software. The next trick is to write out the property in your programming language. People with lots of time and budget can write down enough properties to form a complete specification of the security- and safety-critical parts of a system and prove that they hold for their system. In the talk, we'll instead focus on a dead-simple technique called QuickCheck. (Your programming language almost certainly has a QuickCheck library you can use.) QuickCheck - from the code describing the property - will automatically generate as many test cases as you want, run them, and produce counterexamples for failures. QuickCheck is amazingly effective at flushing out those corner cases that elude traditional unit tests. Finally, for simple properties of pure functions, we can also attempt a proof using simple algebra. The results are a wonderful feeling of satisfaction, and a sound sleep.

Additional information

Type lecture
Language English

More sessions

12/27/19
Resilience & Sustainability
Clarke
Das Umweltbundesamt hat in 2012 mit der Forschung der Umweltrelevanz von Software begonnen. Ziel der Forschung war es, die gegenseitige Beeinflussung von Hard- und Software zu erfassen, zu bewerten und geeignete Maßnahmen zu entwickeln, die es ermöglichen, die Inanspruchnahme von natürlichen Ressourcen durch Software zu reduzieren. Im Vortrag wollen Marina Köhn (Umweltbundesamt) und Dr. Eva Kern (Umwelt-Campus Birkenfeld) die Messergebnisse aus dem Labor der Forschung präsentieren und die ...
12/27/19
Resilience & Sustainability
Julian Oliver
Clarke
In this talk Julian will outline his work as sysadmin, systems and security architect for the climate and environmental defense movement Extinction Rebellion. Responsible for 30 server deployments in 11 months, including a community hub spanning dozens of national teams (some of which operate in extremely hostile conditions), he will show why community-owned free and open source infrastructure is mission-critical for the growth, success and safety of global civil disobedience movements.
12/28/19
Resilience & Sustainability
Chris Adams
Clarke
In this talk, you'll learn about the environmental impact of the digital products and services you build, why this matters. You’ll be introduced to a mental model, known as Platform, Packets, Process, for measuring and identifying emissions hotspots in digital products, and the steps you can take to reduce them.
12/28/19
Resilience & Sustainability
Ada
Deep Learning ist von einem Dead End zur ultimativen Lösung aller Machine Learning Probleme geworden - und einiger anderer auch. Aber wie gut ist dieser Trend wirklich? Und wie nachhaltig? Wir setzen uns mit wissenschaftlicher Nachhaltigkeit, sozialen Auswirkungen, und den Folgen für unsere Ressourcen, unseren Energieverbrauch, und damit unseren Planeten auseinander.
12/28/19
Resilience & Sustainability
Gauthier Roussilhe
Clarke
A lecture on the environmental impacts of digital industry today and how to think about and design digital tools with limited energy and resources.
12/28/19
Resilience & Sustainability
Felix Erdmann
Dijkstra
Der Talk soll die Geschichte der senseBox von Beginn bis jetzt wiedergeben. Dabei möchte ich vor allem auf unsere Arbeit im Bereich Open Source, Open Data, Open Hardware und Open Educational Resources eingehen. Die Motivation von Teilnehmern des senseBox Projekts möchte ich basierend auf einer Nutzerstudie kurz wiedergeben. Außerdem möchte ich auf aktuelle Probleme sowie technische Hürden und die Genauigkeit der Daten eingehen. Zu guter Letzt gebe ich einen kurzen Ausblick in die Zukunft ...
12/28/19
Resilience & Sustainability
Paul Gardner-Stephen
Clarke
Civil society depends on the continuing ability of citizens to communicate with one another, without fear of interference, deprivation or eavesdropping. As the international political climate changes alongside that of our physical climatic environment, we must find ways to create mobile communications systems that are truly resilient and sustainable in the face of such shocks. We have therefore identified a number of freedoms that are required for resilient mobile phones: Energy, Communications, ...