Invited Talk: Falcon: Towards an industrial strength heap analyzer
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 JunDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00
|Invited Talk: Toward Gamification of Proofs about Programs|
Sorin Lerner University of California, San Diego
|Invited Talk: Falcon: Towards an industrial strength heap analyzer|
Xiao Xiao SourceBrella Inc.