Hernan Luis Ponce de Leon
Fantastic beasts and where to find them: Advances and open problems in automatic verification of concurrent applications
Push-button (a.k.a. automatic) verification of concurrent programs has made significant progress in the last decades.
Advances in verification technology (e.g. SMT solvers) enabled not only the adoption of such tools in industry, but also to extend its applicability in the software stack (e.g. tools can now reason about how program behave on different architectures).
The amount of mature tools has also recently increased, as witnessed by the number of participants in the Software Verification Competition.
In the first part of this talk, I will discuss and demo how the concurrency team at DRC makes use of automatic bug hunting tools. But finding bugs is just half of the journey in the quest for getting concurrent programming right.
In the second part I will discuss open challenges in debugging, understanding and fixing concurrent bugs.
Advances in verification technology (e.g. SMT solvers) enabled not only the adoption of such tools in industry, but also to extend its applicability in the software stack (e.g. tools can now reason about how program behave on different architectures).
The amount of mature tools has also recently increased, as witnessed by the number of participants in the Software Verification Competition.
In the first part of this talk, I will discuss and demo how the concurrency team at DRC makes use of automatic bug hunting tools. But finding bugs is just half of the journey in the quest for getting concurrent programming right.
In the second part I will discuss open challenges in debugging, understanding and fixing concurrent bugs.
back to overview
Watch Recording
