About

MVD 2014 is the sixth workshop for the midwest region on hardware and software verification, continuing the tradition begun in 2009.

This year MVD will be hosted by the University of Missouri in Columbia, Missouri on October 3rd and 4th, 2014. We expect talks to begin the morning of the 3rd (a Friday) and finish around 1pm on the 4th.

MVD's primary goals are:

Venue

All talks this year will take place in room 200 of the Reynolds Journalism Institute (RJI) building on the MU campus. See here for more details on the location.

Something to keep in mind when designing slides: instead of a projector and screen, this room is equipped with a "video wall" -- a (very) high-resolution display created by combining nine separate displays. As a result, the bezels of the individual displays will cause visible "seams" in the middle of slides. This can be distracting in certain cases. In order to minimize this effect, consider:

Also, note that slides should be designed for a 16:9 aspect ratio if you'd like them to take up the whole display.

We have a PowerPoint here (courtesy of the people at RJI) that demonstrates some ways of coping with this effect. In these slides, you can enable gridlines that approximate the location of the seams by clicking on View->Guides->Static Guides. But note that this probably only works with PowerPoint.

Accommodations

A block of rooms has been reserved for participants at the Stoney Creek Inn nearby. Attendees wishing to stay there must call the hotel to confirm their reservation. More information on the location and accomodations can be found here.

Registration

Participants should register here.

Submissions

Participants should submit abstracts (and optionally, papers) before September 19, 2014.

Contacts

Please send any questions to Rohit Chadha (chadhar@missouri.edu), Chris Hathhorn (crhr38@mail.missouri.edu), or Adam Procter (adamprocter@mail.missouri.edu).

Venue

The presentations will occur at the Reynolds Journalism Institute (RJI), in the Fred W. Smith Forum located in room 200.

Points of interest:

Accomodations

There is a block of rooms being held for participants at Stony Creek Hotel which may be reserved by phone before September 12. Please mention that you are participating in Midwest Verification Day when making the reservation

Phone: (573) 442-6400. Address: 2601 S Providence Rd, Columbia, MO 65203

Alternative hotels:


Directions to the parking garage from Stoney Creek Inn:

Directions to Stoney Creek Hotel

From St. Louis Lambert Airport.

From Columbia Regional Airport.

From Kansas City International Airport.

Register below.

Please submit your abstract through the EasyChair link below.

MVD'14 abstract submission

Registration: September 10, 2014

Abstract submission: September 10, 2014

Special rates for workshop hotel: September 12, 2014

Schedule

All talks will take place in room 200 of the Reynolds Journalism Institute.

Invited speakers

All talks will take place in room 200 of the Reynolds Journalism Institute.

Stacy Prowell

Title: Verification and Security.

Time: 8:30am on Friday, October 3rd.

Bio: Stacy Prowell is the Chief Cyber Research Scientist for Oak Ridge National Laboratory, where his work focuses on applying high-performance computing and computationally intensive methods to automated reverse engineering, semantic analysis, system composition, and software forensics. Stacy also serves as the program manager for the laboratory's Cybersecurity for Energy Delivery Systems program, and holds a joint appointment in the Electrical Engineering and Computer Science Department at the University of Tennessee. Stacy has managed commercial software development projects and has consulted on the design, development, and testing of applications from consumer electronics to medical scanners.

Mahesh Viswanathan

Title: Reasoning about Stability (slides).

Time: 1:15pm on Friday, October 3rd.

Abstract: Stability is an important property of cyberphysical systems that have a continuous component in their state space. It stipulates that if small deviations from an ideal behavior can be tolerated, then there is a neighborhood around the system's starting state that ensures that all behaviors from this neighborhood remain within the tolerated envelope around the target execution. Stability is the most common fundamental requirement imposed on cyberphysical systems. It is often not just a design goal, but is the principal requirement, so much so that unstable systems are deemed "unusable". However, the analysis of stability properties of a system requires fundamentally new techniques that are different from those used for other traditional properties like safety and liveness. One of the reasons for this is that stability is not bisimulation invariant. The talk will outline some of the principal challenges in the automated analysis of stability.

Bio: Mahesh Viswanathan obtained his bachelor's degree in computer science from the Indian Institute of Technology at Kanpur, and his doctorate from the University of Pennsylvania. He was a post-doctoral fellow at DIMACS with a joint appointment with Telcordia Technologies in 2000-01. Since 2001, he has been on the faculty at the University of Illinois at Urbana-Champaign. His research interests are in the core areas of logic, automata theory, and algorithm design, with applications to the algorithmic verification of cyberphysical and stochastic systems.

Alwyn Goodloe

Alwyn Goodloe

Title: Research in the Verification of Flight-Critical Systems (slides).

Time: 8:30am on Saturday, October 4th.

Abstract: This talk is intended to give an overview of formal verification research applied to the verification of flight-critical systems, primarily focusing on research being conducted at the Safety-Critical Avionics Systems Branch at the NASA Langley Research Center. We first give a very brief introduction to the issues of verification in the context of certification of software in civil aviation. A short survey of research in our group applying formal methods to verify algorithms for air traffic management follows. The remainder of the talk will focus on two ongoing projects. The first is developing new tools for formally analyzing numerical software. The second applies runtime verification to flight-critical systems.

Bio: Alwyn Goodloe is a Research Computer Engineer at NASA's Langley Research Center working in the formal methods group of the Safety Critical Avionics Branch. His work at NASA focuses on assurance of flight-critical systems ranging from air traffic management algorithm to fault-tolerant avionics and verification of numerical software. On really good days he gets to play with little airplanes. He has a Ph.D. in Computer and Information Science from the University of Pennsylvania performed under the direction of Professor Carl A. Gunter, where he focused on formal foundations of network security. He was employed as a staff scientist at the National Institute of Aerospace for three years before joining NASA. Prior to going back to school to obtain his PhD at Penn, he worked for fourteen years in the software industry as a software engineer and IT consultant to various US government agencies.

Torben Amtoft

Torben Amtoft

Title: Program Slicing and its Correctness (slides).

Time: 10:45am on Saturday, October 4th.

Abstract: The goal of program slicing is to remove the parts of a program that are irrelevant in a given context. Slicing has been applied for many purposes, such as compiler optimizations or model checking, but often without a firm semantic foundation.

In this talk we shall explore ways of expressing the correctness of slicing. A key demand is that each observable action of the source program can be simulated by the sliced program (weak correctness), whereas the converse (strong correctness) may or may not be required to hold: slicing may be allowed to remove certain loops.

To ensure correctness, the standard approach has been to require that the slice set is closed under certain dependency relations. A number of dependency relations have been proposed, to handle various correctness demands and various kinds of control flow graphs.

We shall present current work on slicing non-deterministic programs which presents a special challenge; to make the development concrete we shall phrase it for Extended Finite State Machines (EFSMs). We shall show how the notions of "Weak Commitment Closure" (WCC) and "Strong Commitment Closure" (SCC), recently introduced by Danicic et al in order to categorize previous approaches to slicing of deterministic programs, smoothly extend to non-determinism and will guarantee weak, respectively strong, correctness. We shall present algorithms for computing the least slices that are closed under WCC or SCC, and illustrate them by examples.

Bio: Torben Amtoft grew up in Denmark and received his PhD from the University of Aarhus in 1993. Since 2002 he has been at Kansas State University where he is currently an associate professor. For the last 20+ years he has done research in programming languages which has resulted in the publication of 1 monograph, 9 papers in refereed journals, and 18 reviewed conference papers.

In recent years, Amtoft has focused on analyzing how information flows in a program. This has applications to language-based security, where he has developed several logics for checking that secret information is not leaked; the initial work was given the best paper award at SAS'04 (Static Analysis Symposium). Another application is program slicing, where he has investigated its semantic foundation and extended it to handle larger classes of program.

Other talks, in order of appearance

Website by Ben Sammons.