| 8.15-9: | Gathering at MSR Building 99 |
| 9-10.30: | Usability (Chair: Lenore Zuck): |
| Usable Verification: Balancing Thinking and Automation | |
| Putting the User in Usable Verification | |
| Computer-aided reasoning for the Masses | |
| Towards Information-rich User Interface Paradigms for Formal Verification | |
| Towards Checking the Usefulness of Verification Tools | |
| Focus: What makes verification tools more or less usable? How can we measure usability? What is the role of automation versus the human-in-the-loop? How do we target tools to specific user communities: students, beginners, and experts? | |
| 11-12.30: | Verification in the large (Chair: Jeannette Wing): |
| Usable Verification for Useful Systems | |
| What use is verified software? | |
| Towards Scalable Modular Checking of User-defined Properties | |
| Compositional verification | |
| Formal verification at Intel | |
| Focus: What is the role of verification in designing and building reliable systems? How can verification help in decomposing problems and composing solutions? What new ideas are needed to scale up the technology and dial down our ambition for verifying large systems? How do connect verification in the small and in the large? | |
| 2-3.30: | Modeling (Chair: John Rushby): |
| Bridging the Formal Techniques and Model-Driven Engineering Divide | |
| Easing Formal Verification through Domain-Specific Languages | |
| Raising the level of abstraction through partial models | |
| TBA | |
| TBA | |
| Focus: Can we raise the level of abstraction in design? Is model-based engineering the most effective way to gain an audience for verification? How does modeling impact usable verification? How do verification tools make modeling more effective? How can verification technology reshape the design lifecycle? | |
| 4-5.30: | CPS (Chair: John Harrison): |
| Static analysis: Coming out of the niche? | |
| The Challenge of Environment Modeling in Verifying Cyber-Physical Software Systems | |
| Integrative challenges of Cyber-physical systems | |
| Effective verification of Flight Critical Software Systems | |
| Usable Synthesis | |
| Focus: Can principles from software modeling and verification be applied to physical and cyber-physical systems? How can verification technology be more useful in the design and analysis of Cyber-Physical Systems by domain experts? How can verification help non-experts effective at building CP systems? | |
| 6PM: | Dinner (Indian Buffet) |
| 9-10.30: | Inference Tools (Chair: Tom Ball): |
| Learning from an expert's proof AI4FM | |
| Leveraging SMT | |
| Leveraging SMT (contd.) | |
| Unleashing the verification genie in the cloud | |
| Usable Verification of Existential Properties (aka Bug Finding) | |
| Focus: In what ways can improved automation in inference tools help make verification technolog more usable? How can the automation itself be improved to address usability? What are novel ways of combining and delivering inference capabilities? | |
| 11-12.30: | Verification tools (Chair: Alan Hu): |
| Software verification | |
| Continued relevance of Bit-level Verification Research | |
| Matching Logic: A New Program Verification Approach | |
| Tools that explain their failures | |
| Usable Auto-active Verification | |
| Focus: What technologies are succeeding or failing on the usability front? Where are the bottlenecks to usability? Is push-button automation a boon or a bane? Can verification tools deliver better feedback? What experiments can we conduct to gauge usability? How can we embed verification tools into the design lifecycle? | |
| 2-3.30: | Analysis tools (Chair: David Monniaux): |
| Precise and scalable program analysis at NEC | |
| Analysis of Parallel Languages | |
| Separating Functional and Parallel Correctness | |
| User-specified type systems for domain-specific verification | |
| Using Symbolic (Java) PathFinder at NASA | |
| Focus: What will make analysis tools more usable? Should one give up precision to make analysis usable? Can less precise analysis be useful? Can push-button tools be usable? What are new challenge areas for analysis tools? How can analysis tools exploit inference and verification capabilities? | |
| 4-5: | Closing Thoughts: Challenges and Next Steps (Chair: Shankar) |
| Focus: What are the lessons learned? Where has verification technology succeeded or failed? Can we make it more usable for verification experts, domain experts, and students? Are there missed opportunities for exploiting verification in nontraditional domains? Are we doing a poor job of getting the word out? How can we make it easier to develop usable verification technology? What are the big experiments to measure and improve usability? |
The meeting will be held in Microsoft Redmond Building 99.
Directions, maps, and a list of the closest hotels may be found at
http://research.microsoft.com/en-us/labs/redmond/visit.aspx