A Unified Approach to Compositional Software Modelling, Analysis and Verification
Lead Research Organisation:
University of Birmingham
Department Name: School of Computer Science
Abstract
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.
Organisations
People |
ORCID iD |
Dan Ghica (Principal Investigator) |
Publications
Bakewell A
(2010)
Data-abstraction refinement: a game semantic approach
in International Journal on Software Tools for Technology Transfer
Bakewell A
(2009)
Tools and Algorithms for the Construction and Analysis of Systems
Ghica D
(2008)
Angelic semantics of fine-grained concurrency
in Annals of Pure and Applied Logic
Ghica D
(2010)
CONCUR 2010 - Concurrency Theory
Ghica D
(2011)
Geometry of synthesis III
Ghica D
(2011)
Foundations of Software Science and Computational Structures
Ghica D
(2007)
Geometry of synthesis
Ghica D
(2011)
Function interface models for hardware compilation
Ghica D
(2010)
Geometry of Synthesis II: From Games to Delay-Insensitive Circuits
in Electronic Notes in Theoretical Computer Science
Ghica D
(2009)
Clipping: A Semantics-Directed Syntactic Approximation
Ghica D
(2011)
Geometry of synthesis iv
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 | Participation in a guidance/advisory 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 | 09/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 |
Title | SYNTHESIS OF ELECTRONIC CIRCUITS |
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 | US2009158235 |
Protection | Patent granted |
Year Protection Granted | 2009 |
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 |