View Abstraction – A Tutorial (Invited Paper)
We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model
property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical
Burns' mutual exclusion protocol.
program verification
model checking
parameterized systems
1-15
Invited Paper
Parosh A.
Abdulla
Parosh A. Abdulla
Fréderic
Haziza
Fréderic Haziza
Lukáš
Holík
Lukáš Holík
10.4230/OASIcs.SynCoP.2015.1
P. A. Abdulla and G. Delzanno. On the coverability problem for constrained multiset rewriting. In Proc. AVIS'06, 5th Int. Workshop on on Automated Verification of Infinite-State Systems, 2006.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. Counter-example guided fence insertion under tso. In Proc. TACAS '08, 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 7214 of Lecture Notes in Computer Science, 2012.
Parosh Aziz Abdulla, Johann Deneux, and Pritha Mahata. Multi-clock timed networks. In Proc. LICS '04, 20th IEEE Int. Symp. on Logic in Computer Science, pages 345-354, 2004.
Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík. All for the price of few (parameterized verification through view abstraction). In VMCAI, volume 7737 of LNCS, pages 476-495, 2013.
Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, and Ahmed Rezine. An integrated specification and verification technique for highly concurrent data structures. In TACAS, volume 7795 of LNCS, pages 324-338, 2013.
Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. Regular model checking without transducers (on efficient verification of parameterized systems). In Proc. TACAS '07, 13th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 4424 of Lecture Notes in Computer Science, pages 721-736. Springer Verlag, 2007.
Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. Handling parameterized systems with non-atomic global conditions. In Proc. VMCAI '08, 9th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, 2008.
Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In LICS, pages 160-170. IEEE Computer Society, 1993.
Parosh Aziz Abdulla, Axel Legay, Julien d'Orso, and Ahmed Rezine. Simulation-based iteration of tree transducers. In Proc. TACAS '05, 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 3440 of Lecture Notes in Computer Science, 2005.
Parosh Aziz Abdulla and Aletta Nylén. Timed Petri nets and BQOs. In Proc. ICATPN'2001: 22nd Int. Conf. on application and theory of Petri nets, volume 2075 of Lecture Notes in Computer Science, pages 53 -70, 2001.
T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In Berry, Comon, and Finkel, editors, Proc. 13th Int. Conf. on Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 221-234, 2001.
M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. On the verification problem for weak memory models. In POPL, pages 7-18. ACM, 2010.
Bernard Boigelot, Axel Legay, and Pierre Wolper. Iterating transducers in the large. In Proc. 15th Int. Conf. on Computer Aided Verification, volume 2725 of Lecture Notes in Computer Science, pages 223-235, 2003.
A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract regular model checking. In Proc. 16th Int. Conf. on Computer Aided Verification, volume 3114 of Lecture Notes in Computer Science, pages 372-386, Boston, July 2004. Springer Verlag.
D. Dams, Y. Lakhnech, and M. Steffen. Iterating transducers. In G. Berry, H. Comon, and A. Finkel, editors, Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, 2001.
G. Delzanno. Automatic verification of cache coherence protocols. In Emerson and Sistla, editors, Proc. 12th Int. Conf. on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 53-68. Springer Verlag, 2000.
Giorgio Delzanno. Verification of consistency protocols via infinite-state symbolic model checking. In FORTE'00, volume 183 of IFIP Conference Proceedings, pages 171-186. Kluwer, 2000.
J. Esparza and S. Schwoon. A bdd-based model checker for recursive programs. In CAV, volume 2102 of LNCS, pages 324-336. Springer, 2001.
Pierre Ganty, Jean-François Raskin, and Laurent Van Begin. A Complete Abstract Interpretation Framework for Coverability Properties of WSTS. In VMCAI'06, volume 3855 of LNCS, pages 49-64. Springer, 2006.
Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, enlarge and check... made efficient. In CAV'05, volume 3576 of LNCS, pages 394-407. Springer, 2005.
Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, enlarge and check: New algorithms for the coverability problem of wsts. J. Comput. Syst. Sci., 72(1):180-203, 2006.
S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992.
G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7):326-336, 1952.
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. Theoretical Computer Science, 256:93-112, 2001.
Kedar S. Namjoshi. Symmetry and completeness in the analysis of parameterized systems. In VMCAI'07, volume 4349 of LNCS, pages 299-313. Springer, 2007.
A. Pnueli, S. Ruah, and L. Zuck. Automatic deductive verification with invisible invariants. In Proc. TACAS '01, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031, pages 82-97, 2001.
A. Pnueli, J. Xu, and L. Zuck. Liveness with (0,1,infinity)-counter abstraction. In Proc. 14th Int. Conf. on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, 2002.
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding power multiprocessors. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 175-186, 2011.
T. Touili. Regular Model Checking using Widening Techniques. Electronic Notes in Theoretical Computer Science, 50(4), 2001. Proc. of VEPAS'01.
N. Yonesaki and T. Katayama. Functional specification of synchronized processes based on modal logic. In IEEE 6th International Conference on Software Engineering, pages 208-217, 1982.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode