- Home
- Register
- Attend
- Conference Program
- SC15 Schedule
- Technical Program
- Awards
- Students@SC
- Research with SCinet
- HPC Impact Showcase
- HPC Matters Plenary
- Keynote Address
- Support SC
- SC15 Archive
- Exhibits
- Media
- SCinet
- HPC Matters
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
Click here to download .ics calendar file
Click here to download .vcs calendar file
Click here to add event to your Google Calendar
