Category Archives: Computer science

2015 EAPLS Board member elections

EAPLS, the European Association for Programming Languages and Systems, aims to stimulate research in the area of programming languages and systems. Formally inaugurated in 1996, it provides a forum for researchers across the domain, working with related organisations and industry to initiate scientific events and stimulate the exchange of ideas, as well as raising funds, organising conferences and divesting financial support.

I’m standing in the 2015 EAPLS Board elections (current Board members); I believe there is a significant opportunity to rejuvenate the activities of EAPLS and raise its profile: building networks for early career researchers, sponsoring new events/initiatives, engaging with the major conferences and journals in our field, encouraging improved knowledge transfer activities with industry, as well as raising the profile of the wider research areas in both UK and EU funding streams. We can also be more active in the policy space, by highlighting the educational and economic impact of the wider research areas of programming languages and systems.

You can view my full election statement; all EAPLS members (free to join) are eligible to vote, with the election open until 15 April 2015.

Tagged ,

Paper submitted to CAV 2015: “Dear CAV, We Need to Talk About Reproducibility”

Today, me, Ben Hall (Cambridge) and Samin Ishtiaq (Microsoft Research) submitted a paper to CAV 2015, the 27th International Conference on Computer Aided Verification, to be held in San Francisco in July. CAV is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems; the conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation.

In this paper we build upon our recent work, highlighting a number of key issues relating to reproducibility and how they impact on the CAV (and wider computer science) research community, proposing a new model and workflow to encourage, enable and enforce reproducibility in future instances of CAV. We applaud the CAV Artifact Evaluation process, but we need to do more. You can download our arXiv pre-print; the abstract is as follows:

How many times have you tried to re-implement a past CAV tool paper, and failed?

Reliably reproducing published scientific discoveries has been acknowledged as a barrier to scientific progress for some time but there remains only a small subset of software available to support the specific needs of the research community (i.e. beyond generic tools such as source code repositories). In this paper we propose an infrastructure for enabling reproducibility in our community, by automating the build, unit testing and benchmarking of research software.

 
(also see: GitHub repo)

Tagged , , , , ,

The Art of Programming

The best programs are written so that computing machines can perform them quickly and so that human beings can understand them clearly. A programmer is ideally an essayist who works with traditional aesthetic and literary forms as well as mathematical concepts, to communicate the way that an algorithm works and to convince a reader that the results will be correct.

Selected Papers on Computer Science (1996)
Donald Knuth

 

Tagged , ,

Solution: Create unhackable systems

 
Needless to say, this tweet prompted a number of subtle (and not so subtle) responses; it is just vague enough to not be 100% sure he is actually joking (because the software verification problem is trivial, right?).

Did North Korea hack Sony? I doubt it; perhaps it was from an unexpected agent.

N.B. high-profile cosmologists appear to be quite happy to make bold statements to the media on issues well outside of their expertise…

Tagged , , , , ,

Christmas computational complexity

While there are alternative explanations for how the naughty/nice list is generated, hashing is important: Santa could be using a Bloom filter, in which false positive matches are possible, but false negatives are not (i.e. a query returns either “possibly in set” or “definitely not in set”, thus it has a 100% recall rate).

And while we’re on this subject, remember Santa’s delivery route represents a nested Travelling Salesman Problem, compounded by the naughty/nice list changing every year…

(Merry Christmas…and watch out!)

Tagged , , ,

Accepted papers and programme for Recomputability 2014

I am co-chairing Recomputability 2014 next week, an affiliated workshop of the 7th IEEE/ACM International Conference on Utility and Cloud Computing (UCC 2014). The final workshop programme is now available and it will take place on Thursday 11 December in the Hobart Room at the Hilton London Paddington hotel.

I will also be presenting our paper on sharing and publishing scientific models (arXiv), as well as chairing a panel session on the next steps for recomputability and reproducibility; I look forward to sharing some of the outcomes of this workshop over the next few weeks.

The workshop Twitter hashtag is #recomp14; you can also follow the workshop co-chairs: @DrTomCrick and @npch, as well as the main UCC account: @UCC2014_London.

Tagged , , , , ,

Computing research

There is nothing to do with computers that merits a PhD.

Max Newman (1897-1984), as quoted in Alan Turing: The Enigma by Andrew Hodges

 

Tagged , , ,

Come and do a funded PhD with me

Fancy doing a PhD with me at Cardiff Metropolitan University? I have a fully-funded studentship (for UK/EU students) starting in January, in collaboration with HP in Bristol:

The Department of Computing & Information Systems, Cardiff Metropolitan University, is pleased to offer a fully funded PhD Studentship in Provably Optimal Code Generation.

This research project (Scaling Superoptimisation for Enterprise Applications) is part of an on-going strategic collaboration between Cardiff Metropolitan University and Hewlett-Packard in Bristol; HP is a leading technology company that operates in more than 170 countries around the world, providing infrastructure and business offerings that span from handheld devices to some of the world’s most powerful supercomputers.

Applicants must have an excellent first degree in Computer Science, Computer Engineering, Mathematics or a related discipline, with interests/experience at the hardware/software interface and/or in mathematical foundations.

This three year PhD will commence in January 2015. The PhD bursary consists of the standard tuition fee for a Home/EU student (to be £3,760 in 2014/15) and a stipend linked to the minimum amount set annually by Research Councils UK (currently £13,590 p.a.).

Project Context:

Our world is increasingly dependent on the effectiveness and performance of software. Tools and methodologies for creating useful software artefacts have been around for many years, but the scalability of these systems for solving challenging real world problems are — in many important cases — poor. While there are numerous socio-technical issues associated with developing large software systems, there is a significant opportunity to address the optimisation of software in a strategic, adaptable and platform-independent way.

Superoptimisation is an approach to optimising code by aiming for optimality from the outset, rather than as the aggregation of heuristics that are neither intended nor guaranteed to give provable optimality. Building on previous work by Crick et al., this research project will further develop the theoretical foundations of superoptimisation, as well as developing a scalable toolchain for superoptimising enterprise-level software applications.

 
For informal enquiries, please send me an email: tcrick@cardiffmet.ac.uk (but please apply via FindAPhD or here).

Deadline for applications: Friday 31 October.

Tagged , , , ,

Paper submitted to Recomputability 2014: “Share and Enjoy”: Publishing Useful and Usable Scientific Models

Last month, me, Ben Hall, Samin Ishtiaq and Kenji Takeda (all Microsoft Research) submitted a paper to Recomputability 2014, to be held in conjunction with the 7th IEEE/ACM International Conference on Utility and Cloud Computing (UCC 2014) in London in December. This workshop is an interdisciplinary forum for academic and industrial researchers, practitioners and developers to discuss challenges, ideas, policy and practical experience in reproducibility, recomputation, reusability and reliability across utility and cloud computing. It aims to provide an opportunity to share and showcase best practice, as well as to offering a platform to further develop policy, initiatives and practical techniques for researchers in this domain.

In our paper, we discuss a number of issues in this space, proposing a new open platform for the sharing and reuse of scientific models and benchmarks. You can download our arXiv pre-print; the abstract is as follows:

The reproduction and replication of reported scientific results is a hot topic within the academic community. The retraction of numerous studies from a wide range of disciplines, from climate science to bioscience, has drawn the focus of many commentators, but there exists a wider socio-cultural problem that pervades the scientific community. Sharing data and models often requires extra effort, and this is currently seen as a significant overhead that may not be worth the time investment.

Automated systems, which allow easy reproduction of results, offer the potential to incentivise a culture change and drive the adoption of new techniques to improve the efficiency of scientific exploration. In this paper, we discuss the value of improved access and sharing of the two key types of results arising from work done in the computational sciences: models and algorithms. We propose the development of an integrated cloud-based system underpinning computational science, linking together software and data repositories, toolchains, workflows and outputs, providing a seamless automated infrastructure for the verification and validation of scientific models and in particular, performance benchmarks.

 
(see GitHub repo)

Tagged , , , , , ,

Illustrious company

Yesterday, I saw this quote from the blurb for Jamie Bartlett’s new book The Dark Net:

Beyond the familiar online world that most of us inhabit — a world of Google, Hotmail, Facebook and Amazon — lies a vast and often hidden network of sites, communities and cultures where freedom is pushed to its limits, and where people can be anyone, or do anything, they want. A world that is as creative and complex as it is dangerous and disturbing. A world that is much closer than you think.

The dark net is an underworld that stretches from popular social media sites to the most secretive corners of the encrypted web. It is a world that frequently appears in newspaper headlines, but one that is little understood, and rarely explored. The Dark Net is a revelatory examination of the internet today, and of its most innovative and dangerous subcultures: trolls and pornographers, drug dealers and hackers, political extremists and computer scientists, Bitcoin programmers and self-harmers, libertarians and vigilantes.

Based on extensive first-hand experience, exclusive interviews and shocking documentary evidence, The Dark Net offers a startling glimpse of human nature under the conditions of freedom and anonymity, and shines a light on an enigmatic and ever-changing world.

 
Computer science: an innovative and dangerous subculture indeed!

(N.B. I have not read this book)

Come and do a (fully-funded) PhD with me

Fancy doing a PhD with me at Cardiff Metropolitan University? I have a fully-funded studentship (for UK/EU students) starting in September, in collaboration with HP in Bristol:

Scaling Superoptimisation for Enterprise Applications

Our world is increasingly dependent on the effectiveness and performance of software. Tools and methodologies for creating useful software artefacts have been around for many years, but the scalability of these systems for solving challenging real world problems are — in many important cases — poor. While there are numerous socio-technical issues associated with developing large software systems, there is a significant opportunity to address the optimisation of software in a strategic, adaptable and platform-independent way.

Superoptimisation is an approach to optimising code by aiming for optimality from the outset, rather than as the aggregation of heuristics that are neither intended nor guaranteed to give provable optimality. Building on previous work by Crick et al., this research project will further develop the theoretical foundations of superoptimisation, as well as developing a scalable toolchain for superoptimising enterprise-level industrial software applications. This research project is a collaboration between Cardiff Metropolitan University and Hewlett-Packard (HP) in Bristol; HP is a leading technology company that operates in more than 170 countries around the world, providing infrastructure and business offerings that span from handheld devices to some of the world’s most powerful supercomputers.

Applicants must have an excellent first degree in Computer Science, Computer Engineering, Electronics or a related discipline, with interests/experience in compilers, optimisation, logic programming, satisfiability modulo theories and mathematical foundations.

 
For informal enquiries, send me an email: tcrick@cardiffmet.ac.uk (but please apply via FindAPhD or here).

Deadline for applications: Friday 22 August.

Tagged , , , ,

Paper submitted to WSSSPE2: “Can I Implement Your Algorithm?”: A Model for Reproducible Research Software

Yesterday, me, Ben Hall and Samin Ishtiaq (both Microsoft Research Cambridge) submitted a paper to WSSSPE2, the 2nd Workshop on Sustainable Software for Science: Practice and Experiences to be held in conjunction with SC14 in New Orleans in November. As per the aims of the workshop: progress in scientific research is dependent on the quality and accessibility of software at all levels and it is critical to address challenges related to the development, deployment and maintenance of reusable software as well as education around software practices.

As discussed in our paper, we feel this multitude of research software engineering problems are not just manifest in computer science, but also across the computational science and engineering domains (particularly with regards to benchmarking and availability of code). We highlight a number of recommendations to address these issues, as well as proposing a new open platform for scientific software development. You can download our arXiv pre-print; the abstract is as follows:

The reproduction and replication of novel scientific results has become a major issue for a number of disciplines. In computer science and related disciplines such as systems biology, the issues closely revolve around the ability to implement novel algorithms and approaches. Taking an approach from the literature and applying it in a new codebase frequently requires local knowledge missing from the published manuscripts and project websites. Alongside this issue, benchmarking, and the development of fair, and widely available benchmark sets present another barrier. In this paper, we outline several suggestions to address these issues, driven by specific examples from a range of scientific domains. Finally, based on these suggestions, we propose a new open platform for scientific software development which effectively isolates specific dependencies from the individual researcher and their workstation and allows faster, more powerful sharing of the results of scientific software engineering.

 
(see GitHub repo)

Tagged , , , , , ,

Paper at HCII 2014: “Changing Faces: Identifying Complex Behavioural Profiles”

In June, my colleague Giles Oatley presented a joint paper entitled: Changing Faces: Identifying Complex Behavioural Profiles at HCII 2014, the 16th International Conference on Human-Computer Interaction in Crete.

If you do not have institutional access to SpringerLink, especially the Lecture Notes in Computer Science series, you can download our pre-print. The abstract is as follows:

There has been significant interest in the identification and profiling of insider threats, attracting high-profile policy focus and strategic research funding from governments and funding bodies. Recent examples attracting worldwide attention include the cases of Chelsea Manning, Edward Snowden and the US authorities. The challenges with profiling an individual across a range of activities is that their data footprint will legitimately vary significantly based on time and/or location. The insider threat problem is thus a specific instance of the more general problem of profiling complex behaviours. In this paper, we discuss our preliminary research models relating to profiling complex behaviours and present a set of experiments related to changing roles as viewed through large scale social network datasets, such as Twitter. We employ psycholinguistic metrics in this work, considering changing roles from the standpoint of a trait-based personality theory. We also present further representations, including an alternative psychological theory (not trait-based), and established techniques for crime modelling, spatio-temporal and graph/network, to investigate within a wider reasoning framework.

 
(see Publications)

Tagged , , , , ,

Call for Papers: Recomputability 2014

I am co-chairing Recomputability 2014, the first workshop to focus explicitly on recomputability and reproducibility in the context of utility and cloud computing and is open to all members of the cloud, big data, grid, cluster computing and open science communities. Recomputability 2014 is an affiliated workshop of the 7th IEEE/ACM International Conference on Utility and Cloud Computing (UCC 2014), to be held in London in December 2014.

Recomputability 2014 will provide an interdisciplinary forum for academic and industrial researchers, practitioners and developers to discuss challenges, ideas, policy and practical experience in reproducibility, recomputation, reusability and reliability across utility and cloud computing. It will provide an opportunity to share and showcase best practice, as well as to provide a platform to further develop policy, initiatives and practical techniques for researchers in this domain. Participation by early career researchers is strongly encouraged.

Proposed topics of interest include (but are not limited to):

  • infrastructure, tools and environments for recomputabilty and reproducibility in the cloud;
  • recomputability for virtual machines;
  • virtual machines as self-contained research objects or demonstrators;
  • describing and cataloging cloud setups;
  • the role of community/open access experimental frameworks and repositories for virtual machines and data, their operation and sustainability;
  • validation and verification of experimental results by the community;
  • sharing and publication issues;
  • recommending policy changes for recomputability and reproducibility;
  • improving education and training: best practice, novel uses, case studies;
  • encouraging industry’s role in recomputability and reproducibility.

Please see the full call for papers; deadline for submissions (online via EasyChair) is 10 August 2014 17 August 2014.

Tagged , , , , , , ,

Simon Peyton Jones on Teaching Creative Computer Science

An excellent TEDx talk by Simon Peyton Jones, Principal Researcher at Microsoft Research Cambridge and Chair of Computing At School, on why we should teach computer science at school.

Tagged , ,

Alan Turing: mathematician, computer pioneer and code breaker

turingplaque

Found Turing’s plaque today near King’s College, Cambridge (his alma mater).

Tagged ,

2013 ACM Software System Award: Coq

Today, the 2013 ACM Software System Award has been awarded to Bruno Barras, Yves Bertot, Pierre Castéran, Thierry Coquand, Jean-Christophe Filliâtre, Hugo Herbelin, Gerard P. Huet, Chetan Murthy and Christine Paulin-Mohring:

For the Coq Proof Assistant System that provides interactive software for the development of formal proofs, using a powerful logic known as the Calculus of Inductive Constructions.

 
The Coq Proof Assistant System (full award citation), which has been under continuous development for nearly 30 years, is a formal proof management system that supports a rich higher-order logic with powerful inductive definitions. The programming language incorporates a rich dependent type system, applicable to a range of needs from compilers to models of foundational mathematics. Because it can be used to state mathematical theorems and software specifications alike, Coq is a key enabling technology for certified software and has played an influential role in several disciplines including formal methods, programming languages, program verification and formal mathematics. The system is open source, is supported by a substantial and useful library, and has attracted a large and active user community. Since the project started, more than 40 people have contributed various theoretical, implementational and pedagogical works leading to the Coq system as it is now (see Who did What in Coq?).

Some of the significant results that have been accomplished using Coq are: proofs for the four colour theorem, the development of CompCert (a fully verified compiler for C), the development of RockSalt (software-based fault isolation, as used in Google’s Native Client), and most recent, the fully specified and verified hypervisor OS kernel CertiKOS.

(also see: the 2012 recipients, as well as the full chronological listing of awards)

Tagged , , , ,

2013 ACM Turing Award: Lesley Lamport

Today, the 2013 ACM Turing Award has been awarded to Leslie Lamport, Principal Researcher at Microsoft Research:

For fundamental contributions to the theory and practice of distributed and concurrent systems, notably the invention of concepts such as causality and logical clocks, safety and liveness, replicated state machines, and sequential consistency.

 
Lamport has not only advanced the reliability and consistency of computing systems that work as intended (for example, temporal logic of actions (TLA) and Byzantine fault tolerance), but also created LaTeX!

Read the full award citation.

lamport

(also see: the 2012 recipients, as well as the full chronological listing of awards)

Tagged , , ,

2014 IET South Wales Annual Lecture

On Thursday 20th March I will be giving the 2014 IET South Wales Annual Lecture at Swansea University:

Computing: Enabling a Digital Wales

Digital technology (and thus computation) is an indispensable and crucial component of our lives, society and environment. In a world increasingly dominated by technology, we now need to be more than just digitally literate. Across science and engineering, computing has moved on from assisting researchers in doing science, to transforming both how science is done and what science is done. In the context of (Welsh and UK) Government science, technology and innovation policy, computer scientists (of all flavours) have a significant role to play. Tom will ground this hypothesis by describing his research interests at the hardware/software interface, his broader work in education and science policy, and then finishing by presenting a vision for a “Digital Wales” underpinned by science and technology innovation.

 
This talk is free, with registration online.

Tagged , , ,

Paper at AI-2013: “‘The First Day of Summer': Parsing Temporal Expressions with Distributed Semantics”

In December, my PhD student Benjamin Blamey presented a joint paper entitled: ‘The First Day of Summer': Parsing Temporal Expressions with Distributed Semantics at AI-2013, the 33rd SGAI International Conference on Artificial Intelligence in Cambridge.

If you do not have institutional access to SpringerLink, especially the Research and Development in Intelligent Systems series, you can download our pre-print. The abstract is as follows:

Detecting and understanding temporal expressions are key tasks in natural language processing (NLP), and are important for event detection and information retrieval. In the existing approaches, temporal semantics are typically represented as discrete ranges or specific dates, and the task is restricted to text that conforms to this representation. We propose an alternate paradigm: that of distributed temporal semantics –- where a probability density function models relative probabilities of the various interpretations. We extend SUTime, a state-of-the-art NLP system to incorporate our approach, and build definitions of new and existing temporal expressions. A worked example is used to demonstrate our approach: the estimation of the creation time of photos in online social networks (OSNs), with a brief discussion of how the proposed paradigm relates to the point- and interval-based systems of time. An interactive demonstration, along with source code and datasets, are available online.

 
(see Publications)

Tagged , , , , ,
Follow

Get every new post delivered to your Inbox.

Join 366 other followers