Local verification of global invariants in concurrent programs
作者： Ernie Cohen , Michał Moskal , Wolfram Schulte , Stephan Tobies
DOI: 10.1007/978-3-642-14295-6_42
关键词:
摘要: We describe a practical method for reasoning about realistic concurrent programs Our allows global two-state invariants that restrict update of shared state provide simple, sufficient conditions checking those modularly The has been implemented in VCC, an automatic, sound, modular verifier C VCC used to verify functional correctness tens thousands lines Microsoft's Hyper-V virtualization platform and SYSGO's embedded real-time operating system PikeOS.
springer.com
core.ac.uk
sci-hub.st 参考文章(24)
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
Cristiano Calcagno, Hongseok Yang, Peter W. O’Hearn, Computability and Complexity Results for a Spatial Assertion Language for Data Structures FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. ,vol. 2245, pp. 108- 119 ,(2001) , 10.1007/3-540-45294-X_10
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
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies, VCC: A Practical System for Verifying Concurrent C theorem proving in higher order logics. ,vol. 5674, pp. 23- 42 ,(2009) , 10.1007/978-3-642-03359-9_2
K. Rustan M. Leino, Peter Müller, A Basis for Verifying Multi-threaded Programs european symposium on programming. ,vol. 5502, pp. 378- 393 ,(2009) , 10.1007/978-3-642-00590-9_27
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
K. Rustan M. Leino, Peter Müller, Angela Wallenburg, Flexible Immutability with Frozen Objects Verified Software: Theories, Tools, Experiments. pp. 192- 208 ,(2008) , 10.1007/978-3-540-87873-5_17
Xinyu Feng, Rodrigo Ferreira, Zhong Shao, On the relationship between concurrent separation logic and assume-guarantee reasoning european symposium on programming. pp. 173- 188 ,(2007) , 10.1007/978-3-540-71316-6_13
Kim G. Larsen, Ulrik Nyman, Andrzej Wąsowski, On modal refinement and consistency international conference on concurrency theory. pp. 105- 119 ,(2007) , 10.1007/978-3-540-74407-8_8
Viktor Vafeiadis, Matthew Parkinson, A marriage of rely/guarantee and separation logic international conference on concurrency theory. pp. 256- 271 ,(2007) , 10.1007/978-3-540-74407-8_18