Write a Blog >>
LCTES 2018
co-located with PLDI 2018
Tue 19 Jun 2018 16:40 - 16:55 at Discovery AB - WIP paper session

Efficient automatic verification of real world embedded software with numerous properties is a challenge. Existing techniques verify a sufficient subset of properties by identifying implication relations between their verification outcomes. We believe this is expensive and propose a novel complementary approach called grouping. Grouping does not consider the verification outcomes but uses data and control flow characteristics of the program to create disjoint groups of properties verifiable one group at a time.We present three grouping techniques, a framework, and experiments over open source and industrial applications to support our thesis. The experiments show a high gain in performance of a few state-of-the-art tools. This led to the integration of grouping into the verification process of an automotive software manufacturer.

Tue 19 Jun
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

16:10 - 17:25: LCTES 2018 - WIP paper session at Discovery AB
LCTES-2018-papers16:25 - 16:40
Andre Xian Ming ChangFWDNXT and Purdue, Aliasger ZaidyFWDNXT and Purdue, Lukasz BurzawaFWDNXT and Purdue, Eugenio CulurcielloFWDNXT and Purdue
LCTES-2018-papers16:40 - 16:55
Bharti ChimdyalwarTata Consultancy Services, Priyanka DarkeTata Consultancy Services
LCTES-2018-papers16:55 - 17:10
Francisco Sant'AnnaRio de Janeiro State University, Alexandre SztajnbergRio de Janeiro State University, Noemi RodriguezPUC-Rio, Ana Lúcia de Moura
LCTES-2018-papers17:10 - 17:25
Pavan MehrotraStanford University, Sabar DasguptaStanford University, Samantha RobertsonStanford University, Paul NuyujukianStanford University
Link to publication DOI Pre-print Media Attached