Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Tue 17 Jan 2017 15:00 - 15:30 at Amphitheater 44 - Abstract Interpretation Chair(s): Roberto Giacobazzi

Scaling static analysis is one of the main challenges for program verification in general and for abstract interpretation in particular. One way to compactly represent a set of states is using a formula in conjunctive normal form (CNF). This can sometimes save exponential factors. Therefore, CNF formulae are commonly used in manual program verification and symbolic reasoning. However, it is not used in abstract interpretation, due to the complexity of reasoning about the effect of program statements when the states are represented this way. We present algorithms for performing abstract interpretation on CNF formulae recording equality and inequalities of ground terms. Here, terms correspond to the values of variables and of addresses and contents of dynamically allocated memory locations, and thus, a formula can represent pointer equalities and inequalities. The main idea work is the use of the rules of paramodulation as a basis for an algorithm that computes logical consequences of CNF formulae, and the application of the algorithm to perform joins and transformers. The algorithm was implemented and used for reasoning about low level programs. We also show that our technique can be used to implement best transformers for a variant of Connection Analysis via a non-standard interpretation of equality.

Tue 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
Abstract InterpretationVMCAI at Amphitheater 44
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:00
30m
Talk
Complete Abstractions and Subclassical Modal Logics
VMCAI
Vijay D'Silva Google, Marcelo Sousa University of Oxford
14:30
30m
Talk
Structuring Abstract Interpreters through State and Value Abstractions
VMCAI
David Bühler CEA LIST, Boris Yakobowski CEA - LIST, Sandrine Blazy University of Rennes 1, France
Media Attached
15:00
30m
Talk
Conjunctive Abstract Interpretation using Paramodulation
VMCAI
Mooly Sagiv Tel Aviv University, A: Or Ozeri Tel Aviv university, Oded Padon Tel Aviv University, Noam Rinetzky Tel Aviv University
Media Attached