Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017

Statement-wise abstract interpretation that calculates the abstract semantics of a program statement by statement, is scalable but may cause precision loss due to limited local information attached to each statement. While Satisfiability Modulo Theories (SMT) can be used to characterize precisely the semantics of a loop-free program fragment, it is challenging to deal with loops efficiently using plainly SMT formula. In this paper, we propose a block-wise abstract interpretation framework to analyze a program block by block via combining abstract domains with SMT. We first partition a program into blocks, encode the transfer semantics of a block through SMT formula, and at the exit of a block we abstract the SMT formula that encodes the post-state of a block w.r.t. a given pre-state into an abstract element in a chosen abstract domain. We leverage the widening operator of abstract domains to deal with loops. On this basis, we design a disjunctive lifting functor on top of abstract domains to represent and transmit useful disjunctive information between blocks. Furthermore, we consider sparsity inside a large block to improve efficiency of the analysis. Finally, we develop a prototype based on block-wise abstract interpretation. We have conducted experiments on the benchmarks from SV-COMP 2015. Experimental results show that block-wise analysis can check about 1× more properties than statement-wise analysis does.

Mon 16 Jan

VMCAI-2017-papers
16:00 - 17:30: VMCAI - Symbolic analysis and invariant synthesis at Amphitheater 44
Chair(s): Constantin EneaLIAFA, Université Paris Diderot
VMCAI-2017-papers16:00 - 16:30
Talk
VMCAI-2017-papers16:30 - 17:00
Talk
Yakir Vizel, Arie GurfinkelUniversity of Waterloo, Sharon ShohamTel Aviv university, Sharad MalikPrinceton University
VMCAI-2017-papers17:00 - 17:30
Talk
Lukas Holik, Martin HruskaBrno University of Technology , Ondrej LengalBrno University of Technology , Adam RogalewiczBrno University of Technology , Tomas VojnarBrno University of Technology