Automatic software verification and synthesis

Describes developments that Brunel University has made in the area of automatic software verification and synthesis. Their approach is to write specifications in high-order constructive logic map the code into the same logic and use a theorem-prover to prove that the code written in the functional language ML, matches the specification. The paper describes the logic, the theorem-prover and the ML to logic mapping. It also shows how the same theorem-prover can be used to synthesise code from a specification