RESOLVE E-Workshop 2014: Foundations for Automated Verification

Organizers: Joan Krone (Denison), Murali Sitaraman (Clemson), and Bruce W. Weide (Ohio State)

Tentative Agenda

June 16 (Monday)

Session 1: 10:00A - 11:30A

SimpleJava: Powerful expressions are as expressive as simple ones.
Diego Zaccai
Expressions in Java can have very complex effects in a program state, the combination of short-circuit evaluation and functions with side-effects allow. For example, due to the possibility of side-effects in expressions, one can conceive loops where the conditional statement contains all the code needed for the loop (that is, the loop is correct and yet it has no body). Similarly, due to short circuit evaluation one can write a correct recursive function where the only statement of the body contains a recursive call that would only be made if a progress metric was decreased. As a result of this complexity, generating verification conditions (VCs) directly from Java source code would require a too complex a tool. I propose a translation from Java code to JavaSimple, a simpler language that would allow for a simpler VC generator. JavaSimple is not a new language, it a subset of Java where the complexity of expressions is greatly restricted (for example, the use of both the '&&' and '||' operators is forbidden). I will discuss how to translate any Java source to a JavaSimple source as well as a tool that does this automatically.
Progress Towards the Verification of Enterprise Applications
Dustin Hoffman
This talk will summarize progress in developing and using tools and techniques towards realizing the goal of verifying enterprise applications.
Automated Verification Condition Generation for Performance Correctness
Nighat Yasmin
This paper describes an approach for automatically generating verification conditions (VCs) of performance correctness of an implementation. The VCs are based both on specification of functionality and performance profiles of software components.

Session 2: 1:00P - 2:30P

Implementation of an Automated Prover for the RESOLVE Verifying Compiler
Mike Kabbani
In this talk, the techniques used in a working implementation of an integrated VC prover built for the RESOLVE verifying compiler will be discussed and demonstrated. The broad approach approach is based on taking as input a verification condition and a set of theorems, and building a congruence relation between terms.

Session 3: 3:00P - 4:30P

Concurrent Programming in RESOLVE
Murali Sitaraman
The focus of this group discussion will be on suitable constructs for developing and verifying a class of concurrent programs in RESOLVE, where the goal of concurrent computing is to improve performance by leveraging parallel execution potential.

June 17 (Tuesday)

Session 4: 10:00A - 11:30A

Math Type System
Bill Ogden and Blair Durkee

Session 5: 1:00P - 2:30P

A new iteration of RESOLVE to C translation: Progress, challenges, and applications
Dan Welch
This presentation expands upon previous embedded system verification work with the following: 1. A model view controller (MVC)-based implementation of a RESOLVE to C translator. 2. The addition of a new language keyword that allows users to pair RESOLVE specifications with 'external' (non-native RESOLVE) realizations. These developments will be demonstrated on a Telos mote where we formally verify, install, and run a simple driver enhancement using the code generated by our revised tool.
Contributions to Semantic Checking in RESOLVE
Jason Liu
One major feature of RESOLVE is to have a verifying compiler that checks the correctness of a program before running it. In other words, the compiler needs to make sure both the program's syntax and semantics are correct. This talk will focus on checking especially important for beginning RESOLVE programmers, such as to ensure consistency of parameter modes with usage (e.g., preserves mode parameters) and to check that certain language conventions hold (e.g., not calling an external operation in another in the implementation of a data abstraction concept).
Constructing a Specification Website for the RESOLVE Language
Mark Todd
As it stands, the specifications for what is and what is not within the bounds of the RESOLVE language lay scattered across multiple technical reports, research papers and occasionally in unspoken expectations of the professors. The goal of this project is to develop a site that maintains the repository of all of the language's constructs by allowing for simple tools to Create, Update and Destroy the elements of the language and easily access the data. Ultimately, this should be the resource that is the end point of discussion. If something is currently within the bounds of the language, it should be specified explicitly and in great detail within this Specification. This allows everyone to start from the same page of understanding.
A Realization of the Nested List Position Concept
Lingbo Li
This will presentation introduces the concept and its significance as a data structure. Then it presents several key operations and explains how to realize them using a communal implementation.
Developing a "Hands On" Tutorial for RESOLVE
Alex Housand
This research aims to help new users understand the RESOLVE verification system using a hands-on tutorial, similar in the spirit to the Dafny tutorial. The purpose of this talk to share some mock ups of what the end goal is, using an example. I am looking for feedback as to what others think should be included in the tutorial.
RESOLVEā€™s Math Library Expansion and the Proof Checker
Viet Phan
RESOLVE is designed to allow an extensible collection of mathematical theories. This is based on the idea that there will be an automated proof checker on submitted proofs for a new theory and the proofs are written in a standard syntactic form. The syntax is subject to evolution as it depends on the design of the proof checker. My work is to write syntactic proofs for assorted mathematical theories for RESOLVE Math library, including Multiset and Tree theories. As I write proofs, I will be able to give feedback to RSRG regarding the design of the proof checker.

Session 6: 2:30P - 3:00P

Workshop conclusions and future directions

Info:

The workshop will be conducted through a Google hangout and it is free. However, please send a note to Murali Sitaraman (murali at clemson.edu ) if you plan to attend. There will be a hang out hub set up at Clemson, Denison, and Ohio State. Please indicate if you need a separate invitation.

Page last updated Jun 6, 2014