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

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