A verification methodology for model fields
作者： K. Rustan M. Leino , Peter Müller
DOI: 10.1007/11693024_9
关键词:
摘要: … Our contribution in this paper is a verification methodology that solves these problems. The key … We illustrate the problems any verification methodology for model fields has to address in …
springer.com
acm.org
nozdr.ru 参考文章(25)
Frank Piessens, Bart Jacobs, Verifying programs using inspector methods for state abstraction Department of Computer Science, K.U.Leuven, Leuven, Belgium. ,(2005)
Mike Barnett, David A. Naumann, Friends Need a Bit More: Maintaining Invariants Over Shared State mathematics of program construction. pp. 54- 84 ,(2004) , 10.1007/978-3-540-27764-4_5
Ioannis T. Kassios, Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions FM 2006: Formal Methods. pp. 268- 283 ,(2006) , 10.1007/11813040_19
K. Rustan M. Leino, Peter Müller, Object Invariants in Dynamic Contexts european conference on object-oriented programming. ,vol. 3086, pp. 491- 515 ,(2004) , 10.1007/978-3-540-24851-4_22
David R. Cok, Joseph R. Kiniry, ESC/Java2: Uniting ESC/Java and JML Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. pp. 108- 128 ,(2005) , 10.1007/978-3-540-30569-9_6
Yoonsik Cheon, Stephen Edwards, Murali Sitaraman, Gary Leavens, Model variables: cleanly supporting abstraction in design by contract: Research Articles Software - Practice and Experience. ,vol. 35, pp. 583- 599 ,(2005) , 10.1002/SPE.V35:6
Werner Dietl, Peter Müller, Universes: Lightweight Ownership for JML. The Journal of Object Technology. ,vol. 4, pp. 5- 32 ,(2005) , 10.5381/JOT.2005.4.8.A1
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata, Extended static checking for Java Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation - PLDI '02. ,vol. 37, pp. 234- 245 ,(2002) , 10.1145/512529.512558
David A. Naumann, Mike Barnett, Towards imperative modules: reasoning about invariants and sharing of mutable state formal methods. ,vol. 365, pp. 143- 168 ,(2006) , 10.1016/J.TCS.2006.07.035
David Detlefs, Greg Nelson, James B. Saxe, Simplify: a theorem prover for program checking Journal of the ACM. ,vol. 52, pp. 365- 473 ,(2005) , 10.1145/1066100.1066102