AbstractThis paper describes an approach to the semantic analysis of procedural code. The techniques differ from those adopted in current static analysis tools such as MALPAS (Bramson, 1984) and SPADE (Clutterbuck and Carré, 1988) in two key respects: (1) A database is used, together with language‐specific and language‐independent data models, as a repository for all information about a program or set of programs which is required for analysis, and for storing and interrelating the results of analyses; (2) The techniques aim to treat the full language under consideration by a process of successive transformation and abstraction from the source code until a representation is obtained which is amenable to analysis. This abstraction process can include the production of formal specifications from code. The techniques have been partially implemented for the OS/VS IBM diallect of COBOL '74 and for FORTRAN '77. Several components of the resulting toolset have been formally specified in Z, thus meeting some of the integrity requirements for verification tools given in ‘The procurement of safety critical software in defence equipment’ (MoD, 1991). The techniques have been applied in practice to a wide range of source programs and analysis problems (Lano and Haughton, 1993b; Lano, et al., 1991), including assessment problems (Lloyd's Register, 1992, 1993; Hornsby and Eldridge, 1990). Section 1 gives an overview of the analysis process. Section 2 describes the representations used to support the process. Section 3 describes some of the techniques involved, and Section 4 gives examples of applications of the process. The Appendix contains extracts from a large case study carried out using tools developed to support the process.