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

We define and implement a new procedure for automatically checking safety of infinite state systems in a modular way. The main idea is to infer universally quantified procedure summaries which suffice to show the safety property. We assume that the transition system can be modeled as a collection of (possibly mutually recursive) procedures, where the body of each procedure can be described using effectively propositional logic. Our analysis automatically infers universally quantified procedure summaries by using diagrams for generalizations from counterexamples to induction. It is implemented on top of a SAT solver. This procedure is a variant of IC3/PDR approach. We show that the procedure can be used to prove the absence of concurrent modification exceptions in Java programs.

slides (asya_VMCAI.pdf)2.19MiB

Sun 15 Jan

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

10:30 - 12:00
Program AnalysisVMCAI at Amphitheater 44
Chair(s): Boris Yakobowski CEA - LIST
10:30
30m
Talk
Partitioned Memory Models for Program Analysis.
VMCAI
Wei Wang Google, Inc., Clark Barrett Stanford University, Thomas Wies New York University
File Attached
11:00
30m
Talk
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
VMCAI
Asya Frumkin Tel Aviv University, Yotam M. Y. Feldman Tel Aviv University, Ondřej Lhoták University of Waterloo, Canada, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
File Attached
11:30
30m
Talk
Stabilizing Floating-Point Programs using Provenance Analysis
VMCAI
Yijia Gu Northeastern University, Thomas Wahl Northeastern University