Abstract: Fairness for Infinite-State Systems
Authors: Byron Cook, Heidy Khlaaf and Nir Piterman
Paper Information
| Title: | Abstract: Fairness for Infinite-State Systems |
| Authors: | Byron Cook, Heidy Khlaaf and Nir Piterman |
| Proceedings: | WST 2014 Informal Proceedings |
| Editor: | Carsten Fuhs |
| Keywords: | Model Checking, Temporal Logic, Program Analysis, Fair CTL, Fair Termination |
| Abstract: | ABSTRACT. In this paper we introduce the first known tool for symbolically proving fair-CTL properties of (infinite-state) integer programs. Our solution is based on a reduction to existing techniques for fairness-free CTL model checking. The key idea is to use prophecy variables in the reduction for the purpose of symbolically partitioning fair from unfair executions. |
| Pages: | 5 |
| Talk: | Jul 18 08:45 |
| Paper: |  |