Our colleague, Péter Bokor has co-presented a paper at the 13th International Symposium on Automated Technology for Verification and Analysis (October 12–15, 2015, Shanghai, China). The conference promotes research on theoretical and practical aspects of automated analysis, verification and synthesis, by providing a forum for interaction between the regional and the international research communities and industry in the field. This year, four keynote speakers, Martin Fränzle, Joost-Pieter Katoen, Dino Distefano, and J Strother Moore, have shared their in-depth knowledge and insights on the theory and practice of automated analysis and verification of hardware and software systems.

More specifically, efficiency gains are made by defining projections, an adaptation of dynamic program slices, and instructing the bounded model checker to check such projections only. The optimization approach is also proven to be sound, given state properties over a subset of the variables of a program.

Peter and his co-authors also proposed a symbolic encoding of projections and implemented it for a prototype language. The result is a tool called PBMC, which was used for an in-depth efficiency evaluation of the proposed approach, covering a selection of concurrent programs. The results justify the potential of the proposed projection-based technique to significantly improve the efficiency of verification.