Coq Implementation of OO Verification Framework VeriJ
作者： Ke Zhang , Zongyan Qiu
DOI: 10.1007/978-3-319-41591-8_18
关键词:
摘要: We implement an OO specification and verification framework VeriJ in the proof assistant Coq. This covers main features like encapsulation, inheritance polymorphism. It can modularly specify verify programs, while only one per method is necessary. In this paper, we introduce VeriJ, our tool Coq, example to illustrate how specify/verify program a modular abstract way.
springer.com
core.ac.uk
sci-hub.se 参考文章(13)
Qiu Zongyan, Hong Ali, Liu Yijing, Modular verification of OO programs with interfaces international conference on formal engineering methods. pp. 151- 166 ,(2012) , 10.1007/978-3-642-34281-3_13
Matthew Parkinson, Gavin Bierman, Separation logic for object-oriented programming Aliasing in Object-Oriented Programming. ,vol. 7850, pp. 366- 406 ,(2013) , 10.1007/978-3-642-36946-9_13
Andrew McCreight, Practical Tactics for Separation Logic theorem proving in higher order logics. pp. 343- 358 ,(2009) , 10.1007/978-3-642-03359-9_24
Luca Cardelli, Martin Abadi, A Theory of Objects ,(1996)
Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, Frank Piessens, VeriFast: a powerful, sound, predictable, fast verifier for C and java nasa formal methods. ,vol. 6617, pp. 41- 55 ,(2011) , 10.1007/978-3-642-20398-5_4
Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal, Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq Interactive Theorem Proving. pp. 22- 38 ,(2011) , 10.1007/978-3-642-22863-6_5
Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Specification and verification challenges for sequential object-oriented programs verified software theories tools experiments. ,vol. 19, pp. 159- 189 ,(2007) , 10.1007/S00165-007-0026-7
Barbara H. Liskov, Jeannette M. Wing, A behavioral notion of subtyping ACM Transactions on Programming Languages and Systems. ,vol. 16, pp. 1811- 1841 ,(1994) , 10.1145/197320.197383
Matthew J. Parkinson, Gavin M. Bierman, Separation logic, abstraction and inheritance Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '08. ,vol. 43, pp. 75- 86 ,(2008) , 10.1145/1328438.1328451
Dino Distefano, Matthew J. Parkinson J, jStar Proceedings of the 23rd ACM SIGPLAN conference on Object oriented programming systems languages and applications - OOPSLA '08. ,vol. 43, pp. 213- 226 ,(2008) , 10.1145/1449764.1449782