Bibliography on assume-guarantee reasoning of sequential and multithreaded software

• Simulation techniques: Hoare, Milner.
• The Z Specification Language

First-order set based declarative specification language
• Carrol Morgan, Programming from specifications

Defines executable specifications
• JML  Combines executable and declarative specifications for Java
• Axiomatic Semantics for JML
• Using Data Groups to Specify and Check Side Effects
• Local reasoning

Avoid the need for defining heap side-effects using a special logic to describe assertions
• The loop project
• The ESC/2 Java project
• CSSV

Assume-guranantee reasoning using polyhedra abstraction
• The Canvas Project
  Proves correctness of API usage for clients
• Greta's assume-paper
• Modular verification of software components in C,Sagar Chaki and Edmund Clarke and Alex Groce and Somesh Jha and Helmut Veith
• You Assume, We Guarantee: Methodology and Case Studies. T. A. Henzinger, S. Qadeer, S. K. Rajamani, CAV 1998
• Towards Reliable Modular Programs, Rustan Leino, phd thesis.
• A Proof Technique for Rely/Guarantee Properties, Stark, 1985
• A compositional rule for hardware design refinement, McMillan, 1997
• Model Checking and Modular Verification, Grumberg, Long, 1994
• Compositional Model Checking, Clark, Long, McMillan, 1989
• Reactive Modules, Alur, Henzinger 1996
• Conjoining Specifications, Abadi, Lamport, 1995
• Class-Level Modular Analysis for Object Oriented Languages,Francesco Logozzo,SAS 2003
• Assume-guarantee Reasoning for Hierarchical Hybrid Systems, Thomas A. Henzinger, Marius Minea, and Vinayak Prabhu.
• On the Completeness of Compositional Reasoning .ps), Kedar Namjoshi, Richard Trefler, CAV 2000
• Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams (.ps) Kedar Namjoshi, Nina Amla, E. Allen Emerson, and Richard Trefler, TACAS 2001
• Automatic Assume Guarantee Analysis for Assertion-Based Formal Verification
• Thread-modular model checking, C. Flanagan and S. Qadeer, SPIN 2003
• Thread-modular abstraction refinement, T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer CAV 2003
• Thread-Modular Verification For Shared-Memory Programs, Cormac Flanagan, Stephen N. Freund, Shaz Qadeer
• An assume-guarantee rule for checking simulation, Thomas A. Henzinger,Shaz Qadeer,Sriram K. Rajamani,Serdar Tasiran, TOPLAS 2002
• A Behavioral Module System for the Pi-Calculus ,Sriram K. Rajamani and Jakob Rehof, SAS 01 (Behave!)
• Compositional Circular Assume-Guarantee Rules Cannot Be Sound and Complete, Patrick Maier, FOSSACS 2003,
• A Set-Theoretic Framework for Assume-Guarantee Reasoning,Patrick Maier, ICALP 2001,
• A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning,Patrick Maier, PhD Thesis, 2003

• Learning Assumptions for Compositional Analysis, by J.M. Cobleigh, D. Giannakopoulou, and Corina S. Pasareanu, TACAS 2003
• Assume-guarantee verification of source code with design-level assumptions, D. Giannakopoulou, Corina S. Pasareanu, and J.M. Cobleigh, ICSE 2004. 2004.