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.

This talk will summarize progress in developing and using tools and techniques towards realizing the goal of verifying enterprise applications.

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.

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.

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.

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.

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).

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.

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.

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 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.