Selected Extended Papers of VSTTE 2016
This special issue collects current efforts to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation.
Bidirectional Grammars for Machine-Code Decoding and Encoding
Binary analysis, which analyzes machine code, requires a decoder for converting bits into abstract syntax of machine instructions. Binary rewriting requires an encoder for converting instructions to bits. We propose a domain-specific language that ...
Automated Verification of Functional Correctness of Race-Free GPU Programs
We study an automated verification method for functional correctness of parallel programs running on graphics processing units (GPUs). Our method is based on Kojima and Igarashi's Hoare logic for GPU programs. Our algorithm generates verification ...
A Unifying View on SMT-Based Software Verification
After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible ...
Relational Program Reasoning Using Compiler IR
Relational program reasoning is concerned with formally comparing pairs of executions of programs. Prominent examples of relational reasoning are program equivalence checking (which considers executions from different programs) and detecting illicit ...
The Matrix Reproved (Verification Pearl)
In this paper we describe a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum. We present the proof of two variants for the multiplication of matrices: a naive version using three nested loops and ...