Search terms: Results for Poskitt, Christopher M.

Browse by Author

16 Results

Subscribe to RSS feed for this result set

Non-ETH publications are shown. (Hide non-ETH publications)
 

3. A Graph-Based Semantics Workbench for Concurrent Asynchronous Programs

Corrodi, Claudio, Heußner, Alexander and Poskitt, Christopher M. (2016)

A number of novel programming languages and libraries have been proposed that offer simpler-to-use models of concurrency than threads. It is challenging, however, to devise execution models that successfully realise their abstractions without forfeiting performance or introducing...


Conference Contributions

4. The AutoProof Verifier: Usability by Non-Experts and on Standard Code

Furia, Carlo A., Poskitt, Christopher M. and Tschannen, Julian (2015)

Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with reference to AutoProof: a tool that can verify the...


Conference Contributions

5. Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model

Heußner, Alexander, Poskitt, Christopher M., Corrodi, Claudio and Morandi, Benjamin (2015)

To harness the power of multi-core and distributed platforms, and to make the development of concurrent software more accessible to software engineers, different object-oriented concurrency models such as SCOOP have been proposed. Despite the practical importance of analysing SCOOP...


Conference Contributions

7. Verifying Monadic Second-Order Properties of Graph Programs

Poskitt, Christopher M. and Plump, Detlef (2014)

The core challenge in a Hoare- or Dijkstra-style proof system for graph programs is in defining a weakest liberal precondition construction with respect to a rule and a postcondition. Previous work addressing this has focused on assertion languages for first-order properties, which...


Conference Contributions

8. Towards Rigorously Faking Bidirectional Model Transformations

Poskitt, Christopher M., Dodds, Mike, Paige, Richard F. and Rensink, Arend (2014)

Bidirectional model transformations (bx) are mechanisms for automatically restoring consistency between multiple concurrently modified models. They are, however, challenging to implement; many model transformation languages not supporting them at all. In this paper, we propose an...


Conference Contributions

9. Contract-Based General-Purpose GPU Programming

Kolesnichenko, Alexey, Poskitt, Christopher M., Nanz, Sebastian and Meyer, Bertrand (2014)

Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adoption, however, is the difficulty of programming them and the...


Working Papers

External Document (Hide non-ETH publications)

10. Verification of Graph Programs

Poskitt, Christopher M. (2013)


Doctoral Thesis and Habilitation Thesis

11. Applying Search in an Automatic Contract-Based Testing Tool

Kolesnichenko, Alexey, Poskitt, Christopher M. and Meyer, Bertrand (2013)

Automated random testing has been shown to be effective at finding faults in a variety of contexts and is deployed in several testing frameworks. AutoTest is one such framework, targeting programs written in Eiffel, an object-oriented language natively supporting executable pre-...


Conference Contributions

12. Using Contracts to Guide the Search-Based Verification of Concurrent Programs

Poskitt, Christopher M. and Poulding, Simon (2013)

Search-based techniques can be used to identify whether a concurrent program exhibits faults such as race conditions, deadlocks, and starvation: a fitness function is used to guide the search to a region of the program's state space in which these concurrency faults are more likely...


Conference Contributions

13. Verifying Total Correctness of Graph Programs

Poskitt, Christopher M. and Plump, Detlef (2013)

GP 2 is an experimental nondeterministic programming language based on graph transformation rules, allowing for visual programming and the solving of graph problems at a high-level of abstraction. In previous work we demonstrated how to verify graph programs using a Hoare-style...


Conference Contributions

External Document (Hide non-ETH publications)

14. Hoare-Style Verification of Graph Programs

Poskitt, Christopher M. and Plump, Detlef (2012)

GP (for Graph Programs) is an experimental nondeterministic programming language for solving problems on graphs and graph-like structures. The language is based on graph transformation rules, allowing visual programming at a high level of abstraction. In particular, GP frees...


Journal Items

External Document (Hide non-ETH publications)

15. Verification of Graph Programs

Poskitt, Christopher M. (2012)

GP (for Graph Programs) is an experimental nondeterministic programming language which allows for the manipulation of graphs at a high level of abstraction [11]. The program states of GP are directed labelled graphs. These are manipulated directly via the application of...


Conference Contributions

External Document (Hide non-ETH publications)

16. A Hoare Calculus for Graph Programs

Poskitt, Christopher M. and Plump, Detlef (2010)

We present Hoare-style axiom schemata and inference rules for verifying the partial correctness of programs in the graph programming language GP. The pre- and postconditions of this calculus are the nested conditions of Habel, Pennemann and Rensink, extended with expressions for...


Conference Contributions