Pang, Jun ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Liu, Yang; National University of Singapore
Dong, Jinsong; National University of Singapore
External co-authors :
yes
Language :
English
Title :
On combining state space reductions with global fairness assumptions
Publication date :
2011
Event name :
17th International Symposium on Formal Methods
Event place :
Limerick, Ireland
Event date :
2011
Audience :
International
Main work title :
Proc. 17th International Symposium on Formal Methods
Angluin, D., Aspnes, J., Fischer, M.J., Jiang, H.: Self-stabilizing Population Protocols. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol. 3974, pp. 103-117. Springer, Heidelberg (2006)
Bosnacki, D., Dams, D., Holenderski, L.: Symmetric Spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 1-19. Springer, Heidelberg (2000)
Bosnacki, D., Ioustinova, N., Sidorova, N.: Using Fairness to Make Abstractions Work. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 198-215. Springer, Heidelberg (2004)
Bošnački, D.: A light-weight algorithm for model checking with symmetry reduction and weak fairness. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 89-103. Springer, Heidelberg (2003)
Brim, L., Cerná, I., Moravec, P., Simsa, J.: On combining partial order reduction with fairness assumptions. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 84-99. Springer, Heidelberg (2007)
Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. Formal Methods in System Design 9(1-2), 105-131 (1996)
Emerson, E.A., Sistla, A.P.: Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach. ACM Transactions on Programming Languages and Systems 19(4), 617-638 (1997)
Allen Emerson, E., Jha, S., Peled, D.: Combining partial order and symmetry reductions. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 19-34. Springer, Heidelberg (1997)
Fischer, M., Jiang, H.: Self-stabilizing Leader Election in Networks of Finite-State Anonymous Agents. In: Shvartsman, M.M.A.A. (ed.) OPODIS 2006. LNCS, vol. 4305, pp. 395-409. Springer, Heidelberg (2006)
Gyuris, V., Sistla, A.P.:On-the-Fly Model Checking Under Fairness That Exploits Symmetry. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 232-243. Springer, Heidelberg (1997)
Jiang, H.: Distributed Systems of Simple Interacting Agents. PhD thesis, Yale Uni (2007)
Lamport, L.: Proving the Correctness of Multiprocess Programs. IEEE Transactions on Software Engineering 3(2), 125-143 (1977)
Lamport, L.: Fairness and Hyperfairness. Distributed Computing 13(4), 239-245 (2000)
Liu, Y., Pang, J., Sun, J., Zhao, J.H.: Verification of Population Ring Protocols in PAT. In: TASE, pp. 81-89. IEEE, Los Alamitos (2009)
Nitsche, U., Wolper, P.: Relative Liveness and Behavior Abstraction (Extended Abstract). In: PODC, pp. 45-52. ACM, New York (1997)
Peled, D.: Combining Partial Order Reductions with On-the-fly Model-Checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377-390. Springer, Heidelberg (1994)
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409-423. Springer, Heidelberg (1993)
Pnueli, A.: On the Extremely Fair Treatment of Probabilistic Algorithms. In: STOC, pp. 278-290. ACM, New York (1983)
Pnueli, A., Sa'ar, Y.: All you need is compassion. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 233-247. Springer, Heidelberg (2008)
Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1,∞)-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107-122. Springer, Heidelberg (2002)
Pong, F., Dubois, M.: A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems 6(8), 773-787 (1995)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709-714. Springer, Heidelberg (2009)
Sun, J., Liu, Y., Roychoudhury, A., Liu, S., Dong, J.S.: Fair model checking with process counter abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 123-139. Springer, Heidelberg (2009)
Tarjan, R.: Depth-first Search and Linear Graph Algorithms. SIAM Journal on Computing 2, 146-160 (1972)
Ultes-Nitsche, U., James St., S.: Improved Verification of Linear-time Properties within Fairness: Weakly Continuation-closed Behaviour Abstractions Computed from Trace Reductions. Software Testing, Verification & Reliability 13(4), 241-255 (2003)