Plugins for Detecting Deadlocks and Atomicity Violation and Performance Analysis
The talk aims at presenting three plugins being developed at Brno University of Technology. The first one is L2D2, which is a plugin that aims at low-level deadlock detection, in particular, at detecting deadlocks in C programs. The second plugin is Atomer that aims at detecting sequences of calls that are likely to be intended to execute atomically, followed by checking whether they really are always executed atomically. Finally, the third plugin, Looper, aims at automatically deriving conservative complexity bounds. All of the plugins are under active development, but their preliminary experimental evaluation gives quite promising results. The plugins are open source and available through the following web site: http://www.fit.vutbr.cz/research/groups/verifit/tools/sa-plugins/ .
Tue 16 JunDisplayed time zone: Pacific Time (US & Canada) change
07:00 - 09:00 | Session 2Infer Practitioners at Infer Practitioners live stream Chair(s): Nikos Gorogiannis Facebook and Middlesex University London | ||
07:00 45mTalk | Plugins for Detecting Deadlocks and Atomicity Violation and Performance Analysis Infer Practitioners A: Tomas Fiedor VUT Brno, A: Dominik Harmim Brno University of Technology, Faculty of Information Technology, A: Vladimir Marcin Brno University of Technology, Faculty of Information Technology, A: Ondřej Pavela Brno University of Technology, Faculty of Information Technology, A: Adam Rogalewicz Brno University of Technology, Faculty of Information Technology, A: Tomáš Vojnar Brno University of Technology | ||
07:45 45mTalk | Concise Explanations in Static Analysis Driven Code Reviews – Invited Talk Infer Practitioners | ||
08:30 30mCoffee break | Break Infer Practitioners | ||