New Directions In
Software Technology (NDIST '16)

"Transformation-Based Generation of High-Assurance Software"

December 5-8, 2016
St. John, U.S. Virgin Islands
Caneel Bay - Turtle Bay Conference Room

Schedule - Registration

Hotel Accommodations - How to get there

Call for Participation

Transformation-Based Generation of High-Assurance Software

Each year, NDIST has focused on bringing in experts from other fields to introduce new technologies (e.g., synthetic biology) into the discussion of software technology. This year is different: We will focus on core software technologies in which we claim to be true experts, namely the constructive method of software generation.

The constructive method employs sequences of transformation steps to derive programs from machine-amenable specifications. Ideally, each step should be proven. We call such a transformation sequence a derivation. One frequently referenced early example is the thought-piece "Stepwise Program Construction" (Dijkstra, 1968).

Then, many discussion topics arise: To what degree are derivations and proofs automated? What toolkits exist? What is the state of the art? How scalable is the approach? What user skill set is required? What properties are being proved (functional correctness? type correctness? security? termination? resource use?)? Can the starting point be something other than a formal spec (e.g., a sketch)? What about problems with the spec? How can the software integrate with legacy components? How high-level or low-level can the spec be? Does the derivation include algorithm design? How performant can the generated code be? Can many diverse versions be generated automatically? What happens when the spec changes? What about distributed software? How does this process address security?

We will make progress on these and related questions.

Workshop Format:
The workshop program will be divided into half-day sessions focusing on selected challenges. Sessions will include overview presentations and small-group discussions, as well as a hands-on exercise.

Program Chairs: Adam Chlipala Eric Smith General Chair: Cordell Green Steering Committee: Cordell Green Bob Laddaga Pat Lincoln Howie Shrobe