Computer Science ›› 2013, Vol. 40 ›› Issue (10): 148-154.
Previous Articles Next Articles
WAN Liang,SHI Wen-chang and FENG Hui
| [1] Hoare C A R．An Axiomatic Basis for Computer Programming[J]．Communications of the ACM,1969,12(10):576-580 [2] O’Hearn P,Reynolds J,Yang H．Local Reasoning about Programs that Alter Data Structures[C]∥Proceedings of 15th Annual Conference of the European Association for Computer Science Logic．LNCS,Springer-Verlag,2001:1-19 [3] Reynolds J C．Separation logic:A logic for shared mutable data structures.In LICS[C]∥IEEE Computer Society．2002:55-74 [4] Reynolds J C．An overview of separation logic[C]∥ Meyer B,Woodcock J,eds．VSTTE,Lecture Notes in Computer Science．Springer,2005,4171:460-469 [5] O’Hearn P W．Tutorial on separation logic [C]∥ Gupta A,Malik S,eds．CAV．Springer,2008,5123:19-21 [6] Ding L,Dong L D,Piao Y．Deadlock prevention policy of concurrent programming base on Petri net[J]．Journal of Zhejiang University:Science Edition,2012,39(1) [7] Owicki S,Lamport L．Proving liveness properties of concurrent programs[J]．ACM Transactions on Programming Languages and Systems(TOPLAS),1982,4(3):455-495 [8] Kleine M,Bartels B,Gthel T,et al．LLVM2CSP:extracting csp models from concurrent programs[M]．NASA Formal Methods,Springer Berlin Heidelberg,2011:500-505 [9] 肖美华,薛锦云．基于SPIN/Promela 的并发系统验证 [J]．计算机科学,2004,31(8):201-203 [10] Witkowski T,Blanc N,Kroening D,et al．Model checking concurrent linux device drivers[C]∥Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering．ACM,2007:501-504 [11] Grov G,Michaelson G,Ireland A．Formal verification of concurrent scheduling strategies using TLA[C]∥Parallel and Distri-buted Systems,2007International Conference on．IEEE,2007,2:1-6 [12] Apt K R,De Boer F S,Olderog E R．Verification of sequential and concurrent programs[M]．Springer,2010 [13] Feng X,Shao Z,Dong Y,et al．Certifying low-level programs with hardware interrupts and preemptive threads[C]∥PLDI’08:Conference on Programming Language Design and Implementation．ACM,2008:170-182 [14] Feng X,Shao Z,Vaynberg A,et al.Modular verification of assembly code with stack-based control abstractions[C]∥PLDI’06:Conference on Programming Language Design and Implementation．ACM,2006:401-414 [15] Stephan V S,Cristiano C,Bertrand M．Verifying Executable Object-Oriented Specifications with Separation Logic[C]∥24th European Conference．Maribor,Slovenia,June 2010:21-25 [16] Aquinas H,Andrew W A,Francesco Z N．Oracle Semantics for Concurrent Separation Logic[C]∥ESOP．April 2008 [17] Alexey G,Honseok Y．Modular verification of Preemptive OSKernels[C]∥ICEP’11．2011 [18] O’Hearn P W．Resources,concurrency and local reasoning[C]∥Gardner P,Yoshida N,eds．CONCUR,volume 3170of Lecture Notes in Computer Science．Springer,2004:49-67 [19] Yu S W．Formal verification of concurrent programs[D]．Durham University,1999 [20] Brookes S.A semantics for concurrent separation logic[J]．Theor．Computer Science,2007,375:227-270 [21] Hayman J,Winskel G.Independence and concurrent separation logic[C]∥LICS 2006．2006:147-156 |
| No related articles found! |
|
||
Home