A Unified Approach to Compositional Software Modelling, Analysis and Verification

Lead Research Organisation: University of Birmingham
Department Name: School of Computer Science


Software modelling, analysis and verificationcomprises many sophisticated but often disparate techniques such asmodel checking, static analysis or testing. Although takenindividually such techniques are effective in targeting particularproblems, a combined approach is always recommended. However, in theabsence of a unified framework, integration can be awkward and mayfail to achieve true synergy. Using Game Semantics as a commontheoretical foundation we can provide such a unified framework forsoftware modelling, analysis and verification. The modularity ofextant techniques is often limited, which restrains theirscalability. Game Semantics is intrinsically compositional and recentresearch has already shown how it can be used to model subprograms inmodular fashion, especially the subtle interplay between proceduresand state that cannot be represented using extant techniques. However,compositional modelling is only the first step towards compositionalverification. We plan to further develop means for compositionalreasoning, that is methods of specifying properties of executionenvironments and of verifying that subprograms plug together withoutviolating their mutual assumptions. This can be achieved using eitherprogram logics or type systems. Building on existing research, we aimto push compositional methods beyond correctness verification, intomore intensional analyses such as estimating time of execution, memoryrequirements or resource usage. We also aim to expand beyond staticverification, by examining compositional approaches totesting. Throughout the programme, foundational and applied researchwill naturally intertwine and play off each other.


10 25 50

publication icon
Bakewell A (2010) Data-abstraction refinement: a game semantic approach in International Journal on Software Tools for Technology Transfer

publication icon
Ghica D (2008) Angelic semantics of fine-grained concurrency in Annals of Pure and Applied Logic

publication icon
Ghica D (2010) Geometry of Synthesis II: From Games to Delay-Insensitive Circuits in Electronic Notes in Theoretical Computer Science

Description We have discovered the fact that interaction-based semantics (game semantics, geometry of interaction) can be used to give models of programming languages that are both operational (can be executed) and denotational (the meaning of the whole is composed from the meanings of the parts). This properties made such models ideally suited for compositional software analysis and also for circuit synthesis.
Exploitation Route The proof-of-concept compiler and verification tools can be improved in terms of performance and features.
Sectors Digital/Communication/Information Technologies (including Software)

Description The research has been of a theoretical and foundational nature, but it has led to the development of an experimental high-level synthesis compiler made available as an open-source tool. It has been downloaded a few hundred times but we don't know how it has been used.
First Year Of Impact 2012
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Economic,Policy & public services

Description MACDES
Geographic Reach National 
Policy Influence Type Membership of a guidance committee
URL http://www.epsrc.ac.uk/newsevents/pubs/many-core-architectures-and-concurrency-in-distributed-and-em...
Description Advantage Proof of Concept Grant Fund
Amount £15,000 (GBP)
Organisation Advantage West Midlands 
Sector Public
Country United Kingdom
Start 03/2010 
End 04/2010
Description Microsoft Doctoral Fellowship
Amount £60,000 (GBP)
Organisation Microsoft Research 
Department Microsoft Research Cambridge
Sector Private
Country United Kingdom
Start 10/2011 
End 12/2014
Description Spinner
Amount £50,000 (GBP)
Organisation Advantage West Midlands 
Sector Public
Country United Kingdom
Start 01/2007 
End 01/2008
Description The invention relates to a method of synthesising an electronic circuit for performing a function. The method comprises programming the function using a programming language by defining one or more terms, each term comprising one or more functional constants. Game semantics are applied to interpret the programmed function. Each term is interpreted as one or more strategies defined on moves. Each of the constants of the programmed function is associated with a sub-circuit. Each move is associated with at least one input or output port of the associated sub-circuit, and a move occurrence defined by a strategy produces a change of state of an associated port. The associated sub-circuits are combined to provide a synthesised circuit for performing the function. 
IP Reference US8146029 
Protection Patent granted
Year Protection Granted 2012
Licensed No
Impact None
Title GOS 
Description The Geometry of Synthesis is a new approach to higher-level synthesis of VLSI designs ("hardware") from behavioural descriptions written in a conventional ("software") programming language, called Verity. The main difference between GoS/Verity and other HLS tools is full support for functions in the programming language. This allows us to support things like: higher order functions (map, fold), a functional style of programming, recursion, pre-compiled libraries foreign-function interfaces, run-time services, interfacing with legacy IP cores. The output of GoS is generic VHDL which can be (in principle) used in any conventional synthesis or simulation design flow. However, we test and run our code using Altera tool chains and FPGAs. 
Type Of Technology Software 
Year Produced 2010 
Open Source License? Yes  
Impact A few hundred downloads of the tool. 
URL http://www.veritygos.org