7 citations · 12 across the 9 of their papers we have counts for
9 papers
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
Geoffrey W. Hamilton, Temesghen Kahsai, Maurizio Proietti
These proceedings include selected papers presented at the 9th Workshop on Horn Clauses for Verification and Synthesis and the Tenth International Workshop on Verification and Prog…
The Next 700 Program Transformers
Geoffrey Hamilton
In this paper, we describe a hierarchy of program transformers in which the transformer at each level of the hierarchy builds on top of those at lower levels. The program transform…
Tight Polynomial Bounds for Loop Programs in Polynomial Space
A. M. Ben-Amram, G. W. Hamilton
We consider the following problem: given a program, find tight asymptotic bounds on the values of some variables at the end of the computation (or at any given program point) in te…
Distilling Programs to Prove Termination
G. W. Hamilton
The problem of determining whether or not any program terminates was shown to be undecidable by Turing, but recent advances in the area have allowed this information to be determin…
Tight Polynomial Worst-Case Bounds for Loop Programs
Amir M. Ben-Amram, Geoff Hamilton
In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming language - representing non-deterministic imperative programs with bounded loops, and arithmetics lim…
Generating Loop Invariants for Program Verification by Transformation
G. W. Hamilton
Loop invariants play a central role in the verification of imperative programs. However, finding these invariants is often a difficult and time-consuming task for the programmer. W…
Program Transformation to Identify List-Based Parallel Skeletons
Venkatesh Kannan, G. W. Hamilton
Algorithmic skeletons are used as building-blocks to ease the task of parallel programming by abstracting the details of parallel implementation from the developer. Most existing l…
Generating Counterexamples for Model Checking by Transformation
G. W. Hamilton
Counterexamples explain why a desired temporal logic property fails to hold. The generation of counterexamples is considered to be one of the primary advantages of model checking a…
Verifying Temporal Properties of Reactive Systems by Transformation
Geoff Hamilton
We show how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. In particular, we show how the program tr…