Tue 14 Jun 2016 16:15 - 17:00 at San Miguel East - Session IV

Falcon is a path, context, and field sensitive heap analysis engine that can precisely recover the data flow across heap-allocated data structures and answer the load-store matching questions. Falcon employs four design principles to meet the requirement of precisely and efficiently analyzing software that makes extensive use of complex pointer expressions. 1. Modularity – Building memory specification separately for each function and composing the whole program specification from the procedure local specifications. 2. Sparsity – Analyzing each function in a sparse manner to minimize time and memory cost. 3. Staged constraints solving – Customizing a lightweight SMT solver to falsify simple but common path constraints. 4. Demand-driven – Implementing context sensitivity by a cache based on-demand searching to avoid memory explosion in traditional cloning-based approaches. Our experience with Falcon is very encouraging that can successfully help Pinpoint, an industrial strength program verifier, to find deep pointer related bugs with low false-positive rate.

Tue 14 Jun

Displayed time zone: Tijuana, Baja California change

15:30 - 17:00
Session IVSOAP at San Miguel East
15:30
45m
Talk
Invited Talk: Toward Gamification of Proofs about Programs
SOAP
Sorin Lerner University of California, San Diego
16:15
45m
Talk
Invited Talk: Falcon: Towards an industrial strength heap analyzer
SOAP
Xiao Xiao SourceBrella Inc.