Most efforts to automate the formal verification of communicating systems have centred around finite-state systems (FSSs). However, FSSs are incapable of modelling many practical communicating systems, and hence there is interest in a novel class of problems, which we call VIPSs (Value-passing Infinite-state Parameterised Systems). Existing approaches using model checking over FSSs are insufficient for VIPSs, due to their inability both to reason with and about domain-specific theories, and to cope with systems having an unbounded or arbitrary state space. We use the Calculus of Communicating Systems (CCS) with parameterised constants to express and specify VIPSs. We use the laws of CCS to conduct the verification task. This approach allows us to study communicating systems, regardless of their state space, and the data such systems communicate. Automating theorem proving in this system is an extremely difficult task. We provide automated methods for CCS analysis; they are applicable to both FSSs and VIPSs. Adding these methods to the Clam proof-planner, we have implemented an automated theorem prover that is capable of dealing with problems outside the scope of current methods. This paper describes these methods, gives an account as to why they work and provides a short summary of experimental results.

We describe a proof plan that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This plan provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This plan makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate the plan with parts of a substantial example-the synthesis of a unification algorithm.