Document Open Access Logo

View Abstraction – A Tutorial (Invited Paper)

Authors Parosh A. Abdulla, Fréderic Haziza, Lukáš Holík

PDF
Thumbnail PDF

File

OASIcs.SynCoP.2015.1.pdf
  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Author Details

Parosh A. Abdulla
Fréderic Haziza
Lukáš Holík

Cite AsGet BibTex

Parosh A. Abdulla, Fréderic Haziza, and Lukáš Holík. View Abstraction – A Tutorial (Invited Paper). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/OASIcs.SynCoP.2015.1

Abstract

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.
Keywords
  • program verification
  • model checking
  • parameterized systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  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. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In LICS, pages 160-170. IEEE Computer Society, 1993. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. J. Esparza and S. Schwoon. A bdd-based model checker for recursive programs. In CAV, volume 2102 of LNCS, pages 324-336. Springer, 2001. Google Scholar
  19. 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. Google Scholar
  20. 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. Google Scholar
  21. 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. Google Scholar
  22. S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992. Google Scholar
  23. G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7):326-336, 1952. Google Scholar
  24. 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. Google Scholar
  25. Kedar S. Namjoshi. Symmetry and completeness in the analysis of parameterized systems. In VMCAI'07, volume 4349 of LNCS, pages 299-313. Springer, 2007. Google Scholar
  26. 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. Google Scholar
  27. 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. Google Scholar
  28. 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. Google Scholar
  29. T. Touili. Regular Model Checking using Widening Techniques. Electronic Notes in Theoretical Computer Science, 50(4), 2001. Proc. of VEPAS'01. Google Scholar
  30. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact