WIP: Statically Relating Program Properties for Efficient Verification
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 JunDisplayed time zone: Eastern Time (US & Canada) change
16:10 - 17:25 | |||
16:25 15mShort-paper | WIP: Deep Neural Networks compiler for a trace-based accelerator LCTES 2018 Andre Xian Ming Chang FWDNXT and Purdue, Aliasger Zaidy FWDNXT and Purdue, Lukasz Burzawa FWDNXT and Purdue, Eugenio Culurciello FWDNXT and Purdue | ||
16:40 15mShort-paper | WIP: Statically Relating Program Properties for Efficient Verification LCTES 2018 | ||
16:55 15mShort-paper | WIP: Transparent Standby for Low-Power, Resource-Constrained Embedded Systems: A Programming Language-Based Approach LCTES 2018 Francisco Sant'Anna Rio de Janeiro State University, Alexandre Sztajnberg Rio de Janeiro State University, Noemi Rodriguez PUC-Rio, Ana Lúcia de Moura | ||
17:10 15mShort-paper | WIP: An open-source realtime computational platform LCTES 2018 Pavan Mehrotra Stanford University, Sabar Dasgupta Stanford University, Samantha Robertson Stanford University, Paul Nuyujukian Stanford University Link to publication DOI Pre-print Media Attached |