Property Directed Reachability for Proving Absence of Concurrent Modification Errors
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.
Conference DaySun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|Partitioned Memory Models for Program Analysis.|
|Property Directed Reachability for Proving Absence of Concurrent Modification Errors|
Asya FrumkinTel Aviv University, Yotam M. Y. FeldmanTel Aviv University, Ondřej LhotákUniversity of Waterloo, Canada, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv universityFile Attached
|Stabilizing Floating-Point Programs using Provenance Analysis|