Compositionality for Tightly Coupled Systems: A New Application of the Propositions-as-Types Interpretation

This publication has 17 references indexed in Scilit:

• Formal verification of concurrent programs using the Larch prover
  IEEE Transactions on Software Engineering, 1998
• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
  Theoretical Computer Science, 1997
• Invariants, composition, and substitution
  Acta Informatica, 1995
• The temporal logic of actions
  ACM Transactions on Programming Languages and Systems, 1994
• Derivation of concurrent programs: two examples
  Science of Computer Programming, 1992
• Conditional rewriting logic as a unified model of concurrency
  Theoretical Computer Science, 1992
• win and sin : predicate transformers for concurrency
  ACM Transactions on Programming Languages and Systems, 1990
• Mechanically verifying concurrent programs with the Boyer-Moore prover
  IEEE Transactions on Software Engineering, 1990
• Proving the Correctness of Multiprocess Programs
  IEEE Transactions on Software Engineering, 1977
• Verifying properties of parallel programs
  Communications of the ACM, 1976