Input Space Partitioning to Enable Massively Parallel Proof

Abstract

Real-world applications often include large, empirically defined discrete-valued functions. When proving properties about these applications, the proof naturally breaks into one case per entry in the first function reached, and again into one case per entry in the next function, and continues splitting. This splitting yields a combinatorial explosion of proof cases that challenges traditional proof approaches. While each proof case represents a mathematical path from inputs to outputs through these functions, the full set of cases is not available up front, preventing a straightforward application of parallelism. Here we describe an approach that slices the input space, creating a partition based on pre-computed mathematical paths such that each slice has only a small number of proof cases. These slices are amenable to massively parallel proof. We evaluate this approach using an example model of an adaptive cruise control, where proofs are conducted in a highly parallel PVS environment.