Supervisors: Gordon Pace and Sandro Spina

Description: Runtime-verification is a technique used to check the correctness of a program against a set of properties at runtime, by checking that the current execution path actually satisfies the properties, and if not, causes an exception to be raised. Building monitoring code for temporal properties (stating for example, the expected order of execution of methods) in a large project can be a laborious and error-prone task. A programming technique that has been shown to be useful for this task, is aspect-oriented programming, in which the programmer can weave new code into existing programs in an automatic manner.

In this APT, students will build a system to (i) specify properties about the order of execution of methods in a Java program using finite state automata; (ii) use AspectJ (an AOP tool for Java) to weave such properties into a program; and (iii) evaluate their system on a real Java program.

Extensions may include increasing the expressivity of the automata (for example by introducing variables) and providing a more abstract specification language which can be automatically translated into the property automata (for example, regular languages).

References:

• Séverine Colin, Leonardo Mariani, Run-Time Verification, Model-Based Testing of Reactive Systems 2004, 2004.
• Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm and William G. Griswold,An Overview of AspectJ, ECOOP2001, 2001.

Supervisors: Patrick Abela and Gordon Pace

Principal goals of task: Build a domain specific language based on Haskell to describe either business rules or personalization rules, and write tools which analyze the rules and compile these rules to another language (Java code/Microsoft Excel macros).

Description: Domain specific languages are simple languages designed to express succinctly and elegantly tasks for a narrow domain. One problem with designing such a language is that despite their simplicity, one usually has to build a structure above the basic domain-specific language constructs to enable normal programming features such as modularization, iteration, recursion, conditionals, variables, etc.

One solution proposed to minimize this problem is to embed the basic domain specific language within another programming language. When embedding a language one builds a small library to describe, manipulate, and execute the embedded language within another language (called the host language). The programmer can then, using the host language, write programs in the embedded language and use the standard features (such as iteration and conditionals) from the host language.

The aim of the project is to design and develop an embedded language designed for business rules domain which is embeddable within the Java language and Excel scripts.

This project is being organized together with the local companies Ixaris Systems Ltd and CrimsonWing, who will provide test case rules for specific domains (business rules for financial transactions (Ixaris) and personalization rules for customization (Crimsonwing) for which the students will build a combinator library in Haskell to describe the rules in one of these domains. XML input to these rules should also be allowed using HaXml or a similar library. An example of a rule which the user may want to describe is:

If the transient fraud risk is between 1/3 to 2/3 of the max, then we can go ahead with any acquirer (Acquirer:ALL) provided the validation mechanism is 3D-secure plus CVV2 (Validation:3DSecure AND ANYOF{BasicCVV2Check, StrictCVV2Check} ), and provided that the chargeback rate in the month is less than 50% of the threshold (CurrentChargebackRate:LESSTHAN(50%))

The students should then build a simple library to analyze rules described in the language. Analysis can be done via test-case generation, or by manipulating the rules to make them simpler, or find contradictions within them.

Finally, the user should also be allowed to generate a Java class or Excel sheet (with embedded macros) which calculates the output of a rule, which will allow end users to access frequently used rules more easily.

References:

• Paul Hudak, Building Domain-Specific Embedded Languages, ACM Computing Surveys 28A(4), December 1996.
• Simon Peyton Jones (editor), Haskell 98 Language and Libraries: The Revised Report, available from www.haskell.org , December 2002.
• Simon Peyton Jones, Jean-Marc Eber and Julian Seward, Composing contracts: an adventure in financial engineering,, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, 2000.
• Malcolm Wallace and Colin Runciman, Haskell and XML: Generic Combinators or Type-Based Translation?, International Conference on Functional Programming (ICFP '99), 1999.

Supervisors: Joe Cordina, Sandro Spina and Gordon Pace

Principal goals of task: Construct a program that takes a particular theorem formulated as a series of logical statements and is able to automatically perform theorem proofs on these statements.

Description:Having a number of clauses in conjunctive normal form (CNF) where two clauses are the negation of each other obviously shows that the logical statement is unsatisfiable (ex. P & Q & ~P). A theorem is normally formulated as a series of statements that when assumed to be true, the conclusion will follow. By forming the conjunction of the pre-conditions with the negative of the conclusion of the theorem, one might be able to make use of the previous technique to prove by contradiction the theorem. Unfortunately it is very rare that a theorem is made up of simple conjuncted literal terms.

The Tableaux Method is a technique based on the above ideas but making use of a number of rules to express the different ways a contradiction can be discovered when trying to prove a theorem. Your task (as student taking this APT) will be that of understanding the theory behind the tableaux method (we will direct you towards all the relevant literature). Secondly you will build a program that takes a series of logical statements and will apply the tableaux method upon these statements. You will quickly discover that one has often to make decisions on which evaluation path to follow, some of which will lead to a quicker solution than others. Naively one can try evaluating all possible paths, but further reading published papers will lead you to more intelligent approaches to a solution. Alternatively you might like to explore how one might produce a counter-example when a solution does not exist.

And at the end of all this, we will put up online a Hall of Fame for the quickest programs that can solve a series of problems we will provide you with which will include a number of theorems on the Sudoku game!

• Any introductory Texts on the Tableaux Method.
• Reiner Hähnle, Handbook of Automated Reasoning, Chapter 3, pp. 101-178, May 2001, Elsevier Publishers (will give you all the info you need).

Supervisors: Sandro Spina and Gordon Pace

Description: Satisfiability (SAT) addresses the problem of deciding whether a particular Boolean formula in conjunctive normal form (CNF) has an assignment to its terms that makes the formula true. Consider for example the formula (A | B) & (¬A | ¬B | C). The assignment (A=F, B=T, C=F) makes this formula true and we thus say the formula is satisfiable, since there exists at least one assignment which makes the formula true. Now consider the formula (A | B) & (A | ¬B) & (¬A | C) & (¬A | ¬C). There exists no assignment which makes this formula true, hence we say that the formula is not satisfiable.

A number of SAT solving algorithms have been developed over the years. For this APT you are required to implement the following two SAT solvers: (i)The Davis-Putnam (DP) Algorithm (1960) (ii) The Davis-Logemann-Loveland (DLL) Algorithm (1962).

For a successful delivery of the APT, the students are required to fully understand how these two SAT solvers work. Students are required to implement at least the DP SAT solver. Implementation of the DLL algorithm is required for top marks in the APT.

The SAT solvers implemented are to be implemented in an appropriately low-level language such as C to ensure efficiency. The programs should be able to read a formula input as a text file, and output the result of the algorithm, in a simple text only format. The deliverable is to be a command-line program with no fancy graphical user interface. We shall eventually provide a series of Boolean formulae with which students can test their implementation of the SAT solvers.

• M. Davis, H. Putnam, A computing procedure for quantification theory, Journal of ACM, Vol. 7, pp. 201-214, 1960
• M. Davis, G. Logemann and D. Loveland, A Machine Program for Theorem-Proving, Communications of ACM, Vol. 5, No. 7, pp. 394-397, 1962.

Supervisor: Gordon Pace

Principal goals of task: Write a system, which given a collection of hyperlinked documents and a CTL formula, verify whether the formula is satisfied by the documents.

Description: A collection of linked hypermedia documents can be seen as a graph with documents as nodes and links as transitions. Clearly, sometimes one would like to express properties about such systems, such as "wherever I am in the system, I can always navigate back to the index page in less than 2 clicks" or "once I read a page about dogs, pages about cats will no longer be reachable unless I go back through the index page".

Computation Tree Logic (CTL) is a logic which can be used to describe such temporal properties of systems (for example eventuality behaviours) represented as graphs. This makes it ideal to describe certain behaviours we may want to impose on our hypermedia document collection. Furthermore, it has been shown that checking CTL properties on finite graphs is decidable.

The aim of this project may be subdivided into three parts:

• Understanding the underlying notions behind CTL and the verification algorithm used to check properties in this logic. This includes the understanding of certain underlying notions such as graph algorithms to identify strongly connected components.
• Design and implement a simple translator from hyperlinked documents into a graph.
• Design and implement the CTL verification algorithm to be applied to the hyperdocument graphs.

Deliverables: A tool explaining verifying a collection of linked documents with a given CTL property, explaining whether the property is satisfied and, if not, where and how it fails. A report describing the notions behind the algorithms and the design and implementation of the verification procedure and a few examples illustrating how the tool works.

References:

• E. M. Clarke, O. Grumberg and D. A. Peled, Model Checking, MIT Press, ISBN 0-262-03270-8, 1999.
• E. M. Clarke, E. A. Emerson and A. P. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, April 1986.

Supervisors: Kevin Vella and Gordon Pace

Principal goals of task: To construct a compiler from a simple concurrent language to register-level VHDL.

Description: The aim of this project may be subdivided into 3 parts:

• The definition of a simple concurrent language based on Occam, featuring sequential and parallel composition of processes, communication via channels or shared variables, a conditional construct, an iterative construct and non-recursive macros. The student is expected to informally specify the exact semantics of the defined language.
• The design and implementation of a lexical analyser and parser for the above language to transform a given program into its abstract syntax tree representation.
• The design and implementation of the actual compilation stage, which transforms the abstract syntax tree representation into a VHDL representation of synchronous hardware, based on techniques presented in papers cited below. The output should run through a VHDL simulator (freely downloadable) to validate compiler correctness.

• INMOS Ltd., Occam 2 Reference Manual, Prentice Hall, 1988.
• Niklaus Wirth, Hardware Compilation: Translating Programs Into Circuits, IEEE Computer, 31(6), pp 25-31. June 1998.
• Ian Page and Wayne Luk, Compiling Occam into field-programmable gate arrays, FPGAs, Oxford Workshop on Field Programmable Logic and Applications, 1991.
• Gordon Pace and Koen Claessen, An Embedded Language Approach to Teaching Hardware Compilation, SIGPLAN Notices 37(12): 35-46, 2002
• Roger Lipsett, Erich Marchner, and Moe Shahdad, VHDL the language, IEEE Design and Test, 3(2):28-41, April 1986.

Supervisor: Gordon Pace

Principal goals of task: The goal of this APT is to develop a Binary Decision Diagram library and a front end using the library to verify safety properties of synchronous circuits.

Description: Various applications require the storing and manipulation of boolean propositions. Manipulation varies from taking the conjunction of expressions to the comparison of two boolean expressions. This problem is known to be an NP-complete one, but various algorithms which work reasonably well in practice have been proposed. Binary Decision Diagrams (BDDs) are one such technique.

Consider internally storing a boolean expression as text. Although taking conjunction, disjunction or any other operator on such a representation is easy and efficient, how can the expressions be compared? Comparing the truth table of the expressions is always exponentially hard, which is undesirable. Essentially, BDDs are a data structure which stores a boolean formula, with the added bonus that checking whether a formula is a tautology (always true) or equivalent to another formula takes constant time to evaluate. So where's the catch? The BDD describing a formula can be exponentially big with respect to the length of the formula. However, in practice, BDDs manage to describe a substantial number of interesting formulae in a compact manner.

The behaviour of synchronous (clocked) hardware circuits over time can be described very easily using boolean formulae. Furthermore, one can manipulate these formulae to check whether the circuit complies to a given specification.

Safety properties are a particular class of properties which correspond the informal notion of 'nothing bad ever happens'. One interesting thing about this class of properties, is that they can be expressed using an observer - another circuit which takes as input the input of the original circuit and the output, and checks for correctness, outputting just one boolean value saying whether or not the original circuit is working correctly.

• Henrik Reif Anderson, An Introduction to Binary Decision Diagrams, Lecture Notes for 49285 Advanced Algorithms E97, Technical University of Denmark, 1997. Available from here.
• Randal E. Bryant, Symbolic {Boolean} Manipulation with Ordered Binary-Decision Diagrams, ACM Computing Surveys, volume 24, number 3, 293-318, 1992.
• N. Halbwachs, F. Lagnier and P. Raymond, Synchronous observers and the verification of reactive systems, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, 1993.
• E.M.Clarke, O. Grumberg, D.E. Long, Verification Tools for Finite-State Concurrent Systems, LNCS 803, in the proceedings of REX school/symposium on A decade of concurrency: reflections and perspectives, Noordwijkerhout, The Netherlands, June 1993.