Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Sun 15 Jan 2017 10:30 - 11:00 at Amphitheater 44 - Program Analysis Chair(s): Boris Yakobowski

Scalability is a key challenge in static analysis. For imperative languages like C, the approach taken for modeling memory can play a significant role in scalability. In this paper, we explore a family of memory models called partitioned memory models which divide memory up based on the results of a points-to analysis. We review Steensgaard’s original and field-sensitive points-to analyses and Data Structure Analysis (DSA), and introduce a new cell-based points-to analysis which further extends the benefit of field-sensitive analysis to heap data structures and type-unsafe operations like pointer arithmetics and pointer casting. We give experimental results on benchmarks from the software verification competition using the program verification framework in Cascade. We show that the partitioned memory model built on the cell-based points-to analysis significantly reduces the verification time for programs compared with models built on other analyses.

slides (partitionedmain.pdf)472KiB

Sun 15 Jan

VMCAI-2017-papers
10:30 - 12:00: VMCAI - Program Analysis at Amphitheater 44
Chair(s): Boris YakobowskiCEA - LIST
VMCAI-2017-papers148447260000010:30 - 11:00
Talk
Wei WangGoogle, Inc., Clark BarrettStanford University, Thomas WiesNew York University
File Attached
VMCAI-2017-papers148447440000011:00 - 11:30
Talk
Asya FrumkinTel Aviv University, Yotam FeldmanTel Aviv University, Ondřej LhotákUniversity of Waterloo, Canada, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
File Attached
VMCAI-2017-papers148447620000011:30 - 12:00
Talk
Yijia GuNortheastern University, Thomas WahlNortheastern University