Abstract

This project studied the feasibility of integrating the capabilities of the D-Wave adiabatic quantum annealing processor into a Model Checking MC approach based on Counter-example Guided Abstraction Refinement CEGAR. The computational bottleneck of this approach is the solution of certain combinatorial optimization problems for which the D-Wave processor was specifically designed. We developed a set of tools to sidestep the restrictions imposed by the limited connectivity of the processor, performed a set of benchmarking tests of the device, and implemented a proof of concept example that integrated the quantum processor with regular model checking techniques.

Date

2014

Authors

Federico M Spedalieri, John Damoulakis

Issue

AFRLRIRSTR2014193