Abstract
We present an imperative refinement language for the development of backtracking programs and discuss its semantic foundations. For expressivity, our language includes prospective values and preference — the latter being a variant of Nelson’s biased choice that backtracks from infeasibility of a continuation. Our key contribution is to examine feasibility-preserving refinement as a basis for developing backtracking programs, and several key refinement laws that enable compositional refinement in the presence of non-monotonic program combinators.
Related
Alexandra Mendes
Assistant Professor
My research focuses on encouraging a wider adoption of software verification by creating tools and methods that hide the complexities of verifying software. Recently, I started work on usable security, in particular on the impact of formal verification on the use and adoption of formally verified security software products. Much of my most recent work overlaps with the area of software engineering. For more details, see selected publications and some of my projects. Follow me on Twitter or add me on LinkedIn.