Book,
Concurrency verification: introduction to compositional and noncompositional methods
Cambridge University Press, New York, NY, USA, (2001)
Abstract
This is a systematic and comprehensive introduction both to compositional proof methods for the state-based verification of concurrent programs, such as the assumption-commitment and rely-guarantee paradigms, and to noncompositional methods, whose presentation culminates in an exposition of the communication-closed-layers (CCL) paradigm for verifying network protocols. CITED BY 22 Fei Xie , James C. Browne, Verified systems by composition from verified components, ACM SIGSOFT Software Engineering Notes, v.28 n.5, September 2003 Monika Solanki , Antonio Cau , Hussein Zedan, Augmenting semantic web service descriptions with compositional specification, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, ACM SIGPLAN Notices, v.39 n.9, September 2004 Wim H. Hesselink, Eternity variables to prove simulation of specifications, ACM Transactions on Computational Logic (TOCL), v.6 n.1, p.175-201, January 2005 Gregor Gössler , Joseph Sifakis, Composition for component-based modeling, Science of Computer Programming, v.55 n.1-3, p.161-183, March 2005 Michael Compton, Stenning's protocol implemented in UDP and verified in Isabelle, Proceedings of the 2005 Australasian symposium on Theory of computing, p.21-30, January 01, 2005, Newcastle, Australia Michel Charpentier, Composing invariants, Science of Computer Programming, v.60 n.3, p.221-243, May 2006 Jozef Hooman , Jaco van de Pol, Semantic models of a timed distributed dataspace architecture, Theoretical Computer Science, v.331 n.2-3, p.291-323, 25 February 2005 Claudio de la Riva , Javier Tuya, Automatic generation of assumptions for modular verification of software specifications, Journal of Systems and Software, v.79 n.9, p.1324-1340, September 2006 Miquel Bertran , Francesc Babot , August Climent, Formal Sequentialization of Distributed Systems via Program Rewriting, Electronic Notes in Theoretical Computer Science (ENTCS), 188, p.53-75, July, 2007 Nick Moffat , Michael Goldsmith, Assumption-Commitment Support for CSP Model Checking, Electronic Notes in Theoretical Computer Science (ENTCS), 185, p.121-137, July, 2007 Suzana Andova , Cas Cremers , Kristian Gjøsteen , Sjouke Mauw , Stig F. Mjølsnes , Saša Radomirović, A framework for compositional verification of security protocols, Information and Computation, v.206 n.2-4, p.425-459, February, 2008 André Platzer, Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.6, p.63-77, June, 2007 Carlo A. Furia , Matteo Rossi , Dino Mandrioli , Angelo Morzenti, Automated compositional proofs for real-time systems, Theoretical Computer Science, v.376 n.3, p.164-184, May, 2007 C. B. Jones, Splitting atoms safely, Theoretical Computer Science, v.375 n.1-3, p.109-119, May, 2007 Dimitra Giannakopoulou , Corina S. Păsăreanu , Howard Barringer, Component Verification with Automatically Generated Assumptions, Automated Software Engineering, v.12 n.3, p.297-320, July 2005 Dilian Gurov , Marieke Huisman , Christoph Sprenger, Compositional verification of sequential programs with procedures, Information and Computation, v.206 n.7, p.840-868, July, 2008 Domenico Bianculli , Carlo Ghezzi, Towards a methodology for lifelong validation of service compositions, Proceedings of the 2nd international workshop on Systems development in SOA environments, May 11-11, 2008, Leipzig, Germany Nick Moffat , Michael Goldsmith, Assumption---Commitment Support for CSP Model Checking, Journal of Automated Reasoning, v.41 n.3-4, p.365-398, November 2008 Xinyu Feng, Local rely-guarantee reasoning, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA Ariel Cohen , Kedar S. Namjoshi, Local proofs for global safety properties, Formal Methods in System Design, v.34 n.2, p.104-125, April 2009 Marieke Huisman , Dilian Gurov, Composing Modal Properties of Programs with Procedures, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.7, p.87-101, April, 2009 INDEX TERMS Primary Classification: D. Software D.2 SOFTWARE ENGINEERING D.2.4 Software/Program Verification
