sponsored byACMIEEE The International Conference for High Performance 
Computing, Networking, Storage and Analysis
FacebookTwitterGoogle PlusLinkedInYouTubeFlickr

SCHEDULE: NOV 15-20, 2015

When viewing the Technical Program schedule, on the far righthand side is a column labeled "PLANNER." Use this planner to build your own schedule. Once you select an event and want to add it to your personal schedule, just click on the calendar icon of your choice (outlook calendar, ical calendar or google calendar) and that event will be stored there. As you select events in this manner, you will have your own schedule to guide you through the week.

CIVL: The Concurrency Intermediate Verification Language

SESSION: Programming Tools

EVENT TYPE: Papers

EVENT TAG(S): Programming Systems

TIME: 10:30AM - 11:00AM

SESSION CHAIR(S): Thomas Fahringer

AUTHOR(S):Stephen F. Siegel, Manchun Zheng, Ziqing Luo, Timothy K. Zirkel, Andre V. Marianiello, John G. Edenhofner, Matthew B. Dwyer, Michael S. Rogers

ROOM:18AB

ABSTRACT:

There are numerous ways to express parallel programs: message-passing libraries (MPI) and multithreading and GPU language extensions such as OpenMP, Pthreads, and CUDA, are but a few. This multitude creates a serious challenge for developers of software verification tools: it takes enormous effort to develop such tools, but each development effort typically targets one small part of the concurrency landscape, with little sharing of techniques and code among efforts.

To address this problem, we have developed CIVL: the Concurrency Intermediate Verification Language. CIVL provides a general concurrency model which can represent programs in a variety of concurrency dialects, including those listed above.

The CIVL framework includes a tool, based on model checking and symbolic execution, that can verify the absence of deadlocks, race conditions, assertion violations, illegal pointer dereferences and arithmetic, memory leaks, divisions by zero, and out-of-bound array indexing. It can also check that two programs are functionaly equivalent.

Chair/Author Details:

Thomas Fahringer (Chair) - University of Innsbruck|

Stephen F. Siegel - University of Delaware

Manchun Zheng - University of Delaware

Ziqing Luo - University of Delaware

Timothy K. Zirkel - University of Delaware

Andre V. Marianiello - University of Delaware

John G. Edenhofner - University of Delaware

Matthew B. Dwyer - University of Nebraska-Lincoln

Michael S. Rogers - University of Nebraska-Lincoln

Add to iCal  Click here to download .ics calendar file

Add to Outlook  Click here to download .vcs calendar file

Add to Google Calendarss  Click here to add event to your Google Calendar


Paper provided by the ACM Digital Library

Paper also available from IEEE Computer Society