VeriFast for java: a tutorial
作者： Jan Smans , Bart Jacobs , Frank Piessens
DOI: 10.1007/978-3-642-36946-9_14
关键词:
摘要: VeriFast is a separation logic-based program verifier for Java. This tutorial introduces the verifier's features step by step.
springer.com
core.ac.uk
sci-hub.st 参考文章(50)
Frank Piessens, Bart Jacobs, Dynamic Owicki-Gries reasoning using ghost fields and fractional permissions Department of Computer Science, K.U.Leuven. ,(2009)
Frank Piessens, Jan Smans, Bart Jacobs, Verification of imperative programs: The VeriFast approach. A draft course text Department of Computer Science, K.U.Leuven. ,(2010)
Philip Wadler, Robert Bruce Findler, Programming Languages and Systems Springer-Verlag GmbH. ,(2009) , 10.1007/978-3-642-00590-9_1
Tony Hoare, An Axiomatic Basis for Computer Programming Communications of The ACM. ,vol. 12, ,(1969)
Thomas Tuerk, A Formalisation of Smallfoot in HOL theorem proving in higher order logics. pp. 469- 484 ,(2009) , 10.1007/978-3-642-03359-9_32
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
Werner Michael Dietl, Universe Types Topology, Encapsulation, Genericity, and Tools ETH. ,(2009) , 10.3929/ETHZ-A-005951213
K. Etessami, Analysis of Recursive Game Graphs Using Data Flow Equations verification model checking and abstract interpretation. pp. 282- 296 ,(2004) , 10.1007/978-3-540-24622-0_23
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Peter O’Hearn, John Reynolds, Hongseok Yang, Local Reasoning about Programs that Alter Data Structures computer science logic. ,vol. 2142, pp. 1- 19 ,(2001) , 10.1007/3-540-44802-0_1