Author name cluster

Mark Harman

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

2 author rows

ICLR Conference 2022 Conference Paper

Leveraging Automated Unit Tests for Unsupervised Code Translation

Baptiste Rozière
Jie Zhang 0050
François Charton
Mark Harman
Gabriel Synnaeve
Guillaume Lample

With little to no parallel data available for programming languages, unsupervised methods are well-suited to source code translation. However, the majority of unsupervised machine translation approaches rely on back-translation, a method developed in the context of natural language translation and one that inherently involves training on noisy inputs. Unfortunately, source code is highly sensitive to small changes; a single token can result in compilation failures or erroneous programs, unlike natural languages where small inaccuracies may not change the meaning of a sentence. To address this issue, we propose to leverage an automated unit-testing system to filter out invalid translations, thereby creating a fully tested parallel corpus. We found that fine-tuning an unsupervised model with this filtered data set significantly reduces the noise in the translations so-generated, comfortably outperforming the state-of-the-art for all language pairs studied. In particular, for Java→Python and Python→C++ we outperform the best previous methods by more than 16% and 24% respectively, reducing the error rate by more than 35%.

Details

TCS Journal 2011 Journal Article

A unifying theory of control dependence and its application to arbitrary program structures

Sebastian Danicic
Richard W. Barraclough
Mark Harman
John D. Howroyd
Ákos Kiss
Michael R. Laurence

There are several similar, but not identical, definitions of control dependence in the literature. These definitions are given in terms of control flow graphs which have had extra restrictions imposed (for example, end-reachability). We define two new generalisations of non-termination insensitive and non-termination sensitive control dependence called weak and strong control-closure. These are defined for all finite directed graphs, not just control flow graphs and are hence allow control dependence to be applied to a wider class of program structures than before. We investigate all previous forms of control dependence in the literature and prove that, for the restricted graphs for which each is defined, vertex sets are closed under each if and only if they are either weakly or strongly control-closed. Low polynomial-time algorithms for producing minimal weakly and strongly control-closed sets over generalised control flow graphs are given. This paper is the first to define an underlying semantics for control dependence: we define two relations between graphs called weak and strong projections, and prove that the graph induced by a set of vertices is a weak/strong projection of the original if and only if the set is weakly/strongly control-closed. Thus, all previous forms of control dependence also satisfy our semantics. Weak and strong projections, therefore, precisely capture the essence of control dependence in our generalisations and all the previous, more restricted forms. More fundamentally, these semantics can be thought of as correctness criteria for future definitions of control dependence.

Details DOI

TCS Journal 2010 Journal Article

A trajectory-based strict semantics for program slicing

Richard W. Barraclough
David Binkley
Sebastian Danicic
Mark Harman
Robert M. Hierons
Ákos Kiss
Mike Laurence
Lahcen Ouarbya

We define a program semantics that is preserved by dependence-based slicing algorithms. It is a natural extension, to non-terminating programs, of the semantics introduced by Weiser (which only considered terminating ones) and, as such, is an accurate characterisation of the semantic relationship between a program and the slice produced by these algorithms. Unlike other approaches, apart from Weiser’s original one, it is based on strict standard semantics which models the ‘normal’ execution of programs on a von Neumann machine and, thus, has the advantage of being intuitive. This is essential since one of the main applications of slicing is program comprehension. Although our semantics handles non-termination, it is defined wholly in terms of finite trajectories, without having to resort to complex, counter-intuitive, non-standard models of computation. As well as being simpler, unlike other approaches to this problem, our semantics is substitutive. Substitutivity is an important property because it greatly enhances the ability to reason about correctness of meaning-preserving program transformations such as slicing.

Details DOI

AAMAS Conference 2009 Conference Paper

Evolutionary Testing of Autonomous Software Agents

Cu D. Nguyen
Anna Perini
Paolo Tonella
Simon Miles
Mark Harman
Michael Luck

A system built in terms of autonomous agents may require even greater correctness assurance than one which is merely reacting to the immediate control of its users. Agents make substantial decisions for themselves, so thorough testing is an important consideration. However, autonomy also makes testing harder; by their nature, autonomous agents may react in diﬀerent ways to the same inputs over time, because, for instance they have changeable goals and knowledge. For this reason, we argue that testing of autonomous agents requires a procedure that caters for a wide range of test case contexts, and that can search for the most demanding of these test cases, even when they are not apparent to the agents’ developers. In this paper, we address this problem, introducing and evaluating an approach to testing autonomous agents that uses evolutionary optimization to generate demanding test cases.

PDF

TCS Journal 2007 Journal Article

Equivalence of linear, free, liberal, structured program schemas is decidable in polynomial time

Sebastian Danicic
Mark Harman
Rob Hierons
John Howroyd
Michael R. Laurence

A program schema defines a class of programs, all of which have identical statement structure, but whose expressions may differ. We define a class of syntactic similarity binary relations between linear structured schemas, which characterise schema equivalence for structured schemas that are linear, free and liberal. In this paper we report that similarity implies equivalence for linear schemas, and that a near-converse holds for schemas that are linear, free and liberal. We also show that the similarity of two linear schemas is polynomial-time decidable. Our main result considerably extends the class of program schemas for which equivalence is known to be decidable, and suggests that linearity is a constraint worthy of further investigation.

Details DOI

TCS Journal 2006 Journal Article

Theoretical foundations of dynamic program slicing

Dave Binkley
Sebastian Danicic
Tibor Gyimóthy
Mark Harman
Ákos Kiss
Bogdan Korel

This paper presents a theory of dynamic slicing, which reveals that the relationship between static and dynamic slicing is more subtle than previously thought. The definitions of dynamic slicing are formulated in terms of the projection theory of slicing. This shows that existing forms of dynamic slicing contain three orthogonal dimensions in their slicing criteria and allows for a lattice-theoretic study of the subsumption relationship between these dimensions and their relationship to static slicing formulations.

Details DOI

TCS Journal 2003 Journal Article

Equivalence of conservative, free, linear program schemas is decidable

Michael R. Laurence
Sebastian Danicic
Mark Harman
Rob Hierons
John Howroyd

A program schema defines a class of programs, all of which have identical statement structures, but whose expressions may differ. We prove that given any two structured schemas which are conservative, linear and free, it is decidable whether they are equivalent.

Details DOI