View: session overviewtalk overview

All times listed are in CET (GMT +1).

All times listed are in CET (GMT +1).

12:00 | Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms ABSTRACT. Dedicated many-core processors such as GPGPUs, enable programmers to design and implement parallel algorithms to optimize performance. The stream compaction and summed-area table algorithms are two examples where parallel versions have been proposed in the literature with substantial speed ups compared to sequential counterparts. Since these two algorithms are widely used, their correctness is of the utmost importance, i.e., the algorithms must be functionally correct and their implementations must be memory safe. These algorithms use the parallel prefix sum algorithm internally. In our previous work, we verified two parallel prefix sum algorithms. In this paper, we show how we can reuse a verified sub-function (i.e., prefix sum) to prove more complicated algorithms (i.e., stream compaction and summed area table) in a modular way with less effort. Moreover, we demonstrate that it is feasible in practice to verify larger case studies by building the verification of the complicated algorithm on top of the basic one. To show the correctness of the algorithms, we use deductive program verification based on permission-based separation logic, which is supported by the program verifier VerCors. To the best of our knowledge, we are the first to verify functional correctness of the parallel stream compaction and summed-area table algorithms for an arbitrary array size, using tool support. |

12:20 | CiMPG+F: A Proof Generator & Fixer-upper for CafeOBJ Specifications ABSTRACT. CafeOBJ is a language for writing formal specifications of software and hardware systems. It implements equational logic by rewriting and has been used to verify properties of systems using both proof scores and theorem proving. In this paper, we present CiMPG+F, an extension of the CafeInMaude interpreter that, for a large class of CafeOBJ specifications, (i) generates complete proofs from scratch and (ii) fixes incomplete proof scores. CiMPG+F allowed us to prove from scratch the correctness of different protocols, giving us confidence in the %applicability of the approach. |

12:40 | Proof-theoretic Conservative Extension of HOL with Ad-hoc Overloading PRESENTER: Arve Gengelbach ABSTRACT. Logical frameworks are often equipped with an extensional mechanism to define new symbols. The definitional mechanism is expected to be conservative, i.e. it shall not introduce new theorems of the original language. The theorem proving framework Isabelle implements a variant of higher-order logic where constants may be ad-hoc overloaded, allowing a constant to have different definitions for non-overlapping types. In this paper we prove soundness and completeness for the logic of Isabelle/HOL with general (Henkin-style) semantics, and we prove model-theoretic and proof-theoretic conservativity for theories of definitions. |

All times listed are in CET (GMT +1).

All times listed are in CET (GMT +1).