Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 11:30 - 12:00 at Sala III - Software Verification and Synthesis Chair(s): Ori Lahav

We introduce and evaluate a novel algorithm for an \iccc{}-style checker that operates entirely at the level of equality with uninterpreted functions (EUF). Our checker, called \euforia{}, targets control properties by treating a program’s data operations/relations as uninterpreted functions/predicates. This results in an EUF abstract transition system that \euforia{} analyzes to either (1) discover an inductive strengthening EUF formula that proves the property or (2) produce an abstract counterexample that corresponds to zero, one, or many concrete counterexamples. Infeasible counterexamples are eliminated by an efficient refinement method that constrains the EUF abstraction until the property is proved or a feasible counterexample is produced. We formalize the EUF transition system, prove our algorithm correct, and demonstrate our results on a subset of benchmarks from the software verification competition (SV-COMP) 2017.

Tue 15 Jan
Times are displayed in time zone: (GMT+01:00) Greenwich Mean Time : Belfast change

11:00 - 12:30: VMCAI 2019 - Software Verification and Synthesis at Sala III
Chair(s): Ori LahavTel Aviv University
VMCAI-201911:00 - 11:30
Viorel Preoteasa, Iulia Dragomir, Stavros TripakisAalto University and UC Berkeley
Link to publication DOI Pre-print File Attached
VMCAI-201911:30 - 12:00
VMCAI-201912:00 - 12:30
Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison