Semantics & Verification Research Group

The Semantics & Verification Research Group focuses on the mathematical foundations of computer science, with a particular interest in the analysis and verification of software and hardware. Safety-Critical systems are ones in which errors can be disastrous: loss of life, major financial losses, etc. Techniques to safeguard against such scenarios are essential for such systems, and while testing of systems can identify problems, especially if done in a rigorous fashion. Formal methods, on the other hand, offer techniques ranging from the description of requirements in a formal notation to allow for rigorous reasoning about them, to techniques for automatic verification of hardware and software. This document gives a list of potential Masters and FYP Projects by members of the group in the field which are on offer for 2009/2010.


Runtime Verification
As software systems grow bigger and more complex, the need for their validation is similarly growing. Over the past decades, program analysis has become an increasingly important and active research area striving towards certified code with the ultimate holy grail of providing a guarantee of the absence of errors from a given system. Though testing and simulation is widely used, formal methods have started playing a more important role in program due to the limited coverage testing provides on large and complex systems. Model checking techniques, in which the whole state space of the system is analysed usually fails to scale up to real-life systems. To address the problem of intractability, an alternative approach which has been developed is that of runtime verification, in which the desired properties are only checked at runtime on the active execution path. Properties are written in a formal logic and then transformed into a runtime monitor which is instrumented with the system to be monitored. Subsequently, the runtime monitor guarantees that the system runs correctly, and triggers an appropriate response if a system property is violated. We have recently developed the LARVA real-time runtime verification tool, around which most of these projects revolve.
  • Title: Combining Runtime Verification with Testing
    Supervisor: Gordon Pace and Christian Colombo
    Description: Runtime verification of programs requires a formal specification of requirements against which the runs of the program can be verified. Testing, on the other hand, requires good knowledge of the program's expected behaviour and usually a manual check to ensure that the behaviour generated by the test cases adheres to the expected behaviour. Thus, runtime verification can help testing in at least two ways: (i) generating test cases to test out the properties of the program (apart from the usual code paths); (ii) automatically verify the outcome of the test cases without any manual intervention. The aim of the project is to explore the relationship between runtime verification and testing and showing this synergy by means of suitable case studies.

  • Title: Optimising Runtime Verification
    Supervisor: Gordon Pace and Christian Colombo
    Description: A recurring concern in runtime verification are the overheads induced by the monitoring and mitigating code. There have been various attempts to lessen this overhead. For example by avoiding memory leaks and monitoring only a sample of the objects requiring monitoring. Yet another possibility is to have a high level of modularity to enabling the monitor to discard unnecessary information when going from one module to another. The aim of this project is to explore ways of optimisation and applying them to the tool Larva, evaluating the approaches taken.

  • Title: Back-And-Forth Monads for Compensations
    Supervisor: Gordon Pace and Christian Colombo
    Description: Monads have been shown to be very useful in structuring programs written in the functional paradigm. For instance, the state monad is typically used to encode, and hide away, a state which is piped along a computation inducing a sequentiality in the code. Compensations have been shown to be a useful programming pattern - in which implicit undoing of actions can take place in the execution of a program. This results in control flow bouncing back and forth in a program. The aim of this FYP is to explore the use of monads to model compensation flows in a program --- executing forward unless an error is encountered and backwards if otherwise.

  • Title: Implementation of a Realtime Runtime-Verification Tool
    Supervisor: Gordon Pace and Christian Colombo
    Description: Description: LARVA [1,2] is a runtime monitoring tool for Java which caters a wide range of properties including real-time. The tool takes a specification written in the LARVA input language and generates the corresponding Java monitoring code. This code can then be used during the execution of a Java system, ensuring its adherence to the represented properties. The current tool is a proof-of-concept prototype implementation, with no efficiency considerations or deployment of optimisation techniques. This project aims at producing a complete reimplementation of LARVA in a modular fashion, with special care to optimise the monitoring code produced. In particular, the use of clocks for real-time properties and channels for communication can be done much more efficiently and accurately than in the current version. Modularity and well-planned architecture are a key factor in this project, since the plan is to have other future projects extend the tool and eventually to make it available as an open-source tool.

    References:
    1. C. Colombo. Practical runtime monitoring with impact guarantees of Java programs with real-time constraints. Master's thesis, University of Malta, 2008.
    2. C. Colombo, G. J. Pace, and G. Schneider. Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties. In FMICS'08, Italy, 2008. To appear in LNCS.

  • Title: Runtime Verification for Web-Service Composition
    Supervisor: Gordon Pace and Christian Colombo
    Description: Composing services can yield complex interaction which may either break the top level constraints or the constraints placed by the individual services. Checking for compatibility of services could be done through the analysis of the code implementing the services. However, in many cases, this may not be accessible, and a black box analysis of the interaction between services using the preconditions on the interaction of the individual services, and the expectations of the top level (composed) service as the runtime-verified properties. In this project, the student will be expected to extend the LARVA system to work on web-services and apply the system on a case-study.

  • Title: Intrusion Detection using Runtime Verification
    Supervisor: Gordon Pace and Christian Colombo
    Description: Security over the internet is a very important topic. With newly emerging technologies and frequent discoveries of vulnerabilities, an online security framework would be very desirable. Such an online framework works in parallel with the system and will monitor, discover and mitigate problems and errors which may arise during normal operation of a web system. Naldurg et al. [1] have shown how the logic Eagle can be used to check for a number of well-known security problems: smurf attacks, cookie stealing, multi-domain buffer overflows, password guessing attacks and port-sweep attacks. The aim of this project would be to show how such attacks can be monitored using the LARVA language, possibly extending it to handle statistics with more ease. Furthermore, other common attacks (e.g. attacks related to backend databases) may also be monitored and a suitable case study can be found to show the usefulness of runtime verification for the web.

    References:
    1. Prasad Naldurg, Koushik Sen and Prasanna Thati, A Temporal Logic Based Framework for Intrusion Detection, FORTE 2004, LNCS 3235, 2004.
    2. David de Frutos-Escrig and Manuel Núnez, Formal Techniques for Networked and Distributed Systems, FORTE 2004, LNCS 3235, 2004.

  • Title: Runtime Verification IDE
    Supervisor: Gordon Pace and Christian Colombo
    Description: The input logic for LARVA is well developed and can be used on real systems. However, the syntax of the language still needs to be refined, and a development environment to simplify its use is also required. In this project, an Eclipse plugin for LARVA will be developed, with visualisation and debugging features, all done in an extensible way to enable future projects to build upon.

Programming Languages
  • Title: Distributed Protocols as behaviours in Erlang
    Supervisor: Adrian Francalanza Description: Erlang[1] is a parallel functional programming language that has been used commercially for a number of years to program highly-reliable distributed systems in the area of telecommunications. Behaviours are widely used, higher-order Erlang mechanisms facilitating code resue and abstraction. In essence, they permits one to decompose her code into modules where, through the use of module interfaces and the novel feature of callback obligations, one can define a form of contract between the module and the module client.
    Behaviours have already been used to great effect in [2] to construct a suite of design patterns for concurrent code . In this project, we seek to extend this work by building a suite of erlang behaviours that facilitate the implementation of distributed algorithms such as 2/3 phase commits and consensus. The added challenge from [2] will be the element of distribution, which is at the heart of these behaviours. This entails for the provison and handling of failures, so as to make these behaviours fault-tolerant. The final artefact is expected to consist of:
    1. A suite of behaviours defining a number of widely used distributed algorithms.
    2. A case-study application that tests and makes use of these behaviours.

    Requirements: Strong interest in distributed programming and functional programming.

    Textbooks and Material:
    • [1] Programming Erlang: Software for a concurrent world, Joe Armostrong, ISBN-10 193435600X
    • [2] Assessing Design Patterns for Concurrency, Fikre Leguesse, BIT Final Year Project, 2009.
    • [3] Distributed Algorithms. Nancy Lynch. ISBN 1-55860-348-4
    • [4] Introduction to Distributed Algorithms. Gerard Tel. ISBN 0-521-7483-8.


  • Title: A Pedagogic graphic Tool for Object-Based Languages
    Supervisor: Adrian Francalanza
    Description: Object-based (prototype-based) languages such as Self[2], Cecil[3], JavaScript[4] and ActionScript[5] are object-oriented language which tend to be simpler and more flexible than their class-based counterparts such as Java and C#. This simplicity and flexibility makes these languages better candidates for teaching core object-oriented concepts and design features such as inheritance, delegation, dynamic dispatch, inheritance embedding, object creation and cloning. For a start, in object-based languages there is a clearer separation between object types(interfaces) and object implementations compared to class-based languages.
    The tasks expected from this project can be decomposed in a number of stages. There first needs to be a survey of the existing object-based languages, categorising them according to their features. Based on this categorisation, two languages exhibiting diverse characteristics will be chosen and a Graphic Development Environment tool will then be implemented for the construction of object-based software for these two chosen languages. This tool will use a graphic notation to describe the object structure of the software system constructed and will be able to produce skeleton code for these two languages from this graphic representation. However, the main aim of this tool will be to bring forth the core object-oriented characteristics of one language compared to the other (eg. dynamic vs static inheritance, inheritance by embedding vs inheritance by delegation).

    Requirements: Strong interest in object-oriented programming languages.

    Textbooks and Material:
    • [1] A Theory of Objects. Martin Abadi and Luca Cardelli. ISBN 0-387-94775-2.
    • [2] The Self Language. http://selflanguage.org/
    • [3] Cecil Home page. http://www.cs.washington.edu/research/projects/cecil/
    • [4] JavaScript: The Definitive Guide. David Flanagan. ISBN 0-596-10199-6.
    • [5] ActionScript Homepage. http://www.actionscript.org/


  • Title: Formalising (aspects of) Erlang
    Supervisor: Adrian Francalanza
    Description: Erlang is a parallel functional programming language that has been used commercially for a number of years to program highly reliable systems in the area of telecommunications. The advent of multicore CPUs has spiralled interest for this language among many programming communities.
    Widely used tutorial books such as [1] give an informal account of the Erlang language and its constructs. This project aims to formalise the behaviour a core subset of the language and compare this formalisation it against the actual Erlang implementation. This should improve the understanding of the language and act as a point of departure for further research relating to the semantics of the language.
    More specifically, the tasks associated with this project are:
    1. Identification of a calculus, ie a core subset of the language which embodies the main features of the language. These would typically include parallelism, the mailbox synchornisation mechanism, and possibly a failure model for the language.
    2. Formalise the behaviour of the calculus using operational rules.
    3. Implement the rules, typically using a language that lends itself well to rapid prototyping (eg. Haskell)
    4. Compare the behaviour of the calculus with that of the actual Erlang implementation through judicious test examples.
    Requirements: Interest in concurrency, programming languages and language design.

    References, Textbooks and other Material:
    1. Programming Erlang: Software for a concurrent world, Joe Armostrong, ISBN: 193435600X


  • Title: Assessing Design Patterns for Concurrency
    Supervisor: Adrian Francalanza
    Description: The recent advent of cheap pervasive multi-core processors has raised concerns across the programming world because most programmers are not able to program adequately these machines and harness their true potential.
    The study of Concurrency is not new. The Process Calculi community has been studying this phenomenon for the last 30 odd years, obtaining various important results. However, these results are often deemed abstract and "removed" for the working programmer. The Systems Programming community have also been successful in this regard. They have had to deal with concurrency since the inception of multiprogramming operating systems and they have constructed software that has stood the test of time (eg. Unix OS). However, the solutions proposed are often deemed too low level in nature.
    The Object-Oriented Programming community, which nowadays is the main programming community, has had to deal with concurrency for some time as well. Interestingly, it has been presenting its solutions as Design Patterns, programming idioms which have proved to be very palatable to programmers. One often wonders whether such an approach leads to solutions that are too centred around the object-oriented paradigm and which do not generalise to other paradigms used for concurrent programming such as message passing. This project aims to investigate this question using a very pragmatic approach. We identify a number of concurrency patterns and try to apply them to a message-passing programming model. We then asses how adequately these patterns adapted to the new programming paradigm. More concretely, the candidate is expected to:
    1. understand and familiarise herself with the concept of design patterns.
    2. Identify a number of patterns used for concurrency.
    3. Identify a language based around message passing such as CML, Occam or Erlang, on which the design patterns will be tested.
    4. Identify a case study to program in this language, while putting these design patterns to use.
    5. Critically asses the applicability and genericity of the patterns backing up this assessment with any experience obtained from the case study.
    Requirements: Strong interest in programming methodologies, software design and concurrency.

    References, Textbooks and other Material:
    1. Design patterns : elements of reusable object-oriented software by Erich Gamma, Richard Helm, Ralph Johnson, John Vlissides. Addison Wesley (1995) ISBN: 0201633612
    2. Design Patterns Explained: A New Perspective on Object-Oriented Design (Software Patterns) (Paperback) by Alan Shalloway, James Trott. Addison Wesley; 2 ed. (2004) ISBN: 0321247140
    3. Head First Design Patterns (Head First) (Paperback) by Eric Freeman, Elisabeth Freeman, Bert Bates, Kathy Sierra, O'Reilly Media, Inc. (2004) ISBN: 0596007124
    4. Pattern-Oriented Software Architecture Volume 2: Patterns for Concurrent and Networked Objects (Hardcover) Douglas Schmidt, Michael Stal, Hans Rohnert, Frank Buschmann, Wiley 1 ed. (2000) ISBN: 0471606952


  • Title: A Pedagogic Tool for Predicate Logic
    Supervisor: Adrian Francalanza
    Description: There are usually two main uses for a logical language.
    1. As a deduction system (or proof system), ie. a system to construct proofs or refutations.
    2. As a vehicle to express statements which receive a meaning when they are given what is called an "interpretation."
    The study of the first use is called Proof Theory and the study of the second use is called Model Theory. It is the interaction between these two aspects which makes logic an interesting and effective tool. In fact, this dual view of logic has had a deep influence on various fields of Computer Science, from Artificial Intelligence, to Model Checking to the study of Programming Languages.
    In this project the candidate is invited to build a pedagogic tool which assists the teaching of these logical concepts. It will initially focus on one of the simplest forms of logic, predicate logic, but may be extended to first order logic. There are various aspects that the tool should be able to cater for and handle adequately, such as the clear delineation between syntax and semantics, the concept of multiple interpretations (models) for the same language (syntax), proof system soundness, proof system completeness, and the axiomatisation of interpretations. The aggregation of a pool of examples highlighting these concepts and used by the tool will be considered a fundamental aspect of the project. The candidate will also be assessed on the understanding of any aspect handled by the tool constructed.
    Requirements: An interest in the formal aspect of computer science. A good grasp of the logic preliminaries introduces in the Discrete Mathematics 1st year course.

    References, Textbooks and other Material:
    1. Logic for Computer Science: Foundations of Automatic Theorem Proving. Jean Gallier, Chapters 3,4. (Out of print, but freely downloadable from http://www.cis.upenn.edu/~jean/gbooks/logic.html)
    2. Logic in Computer Science: Modelling and Reasoning about Systems. Michael Huth, Mark Ryan. Cambridge University Press. ISBN: 052154310X



  • Title: A Visual Editor for Haskell
    Supervisor: Gordon Pace and Sandro Spina
    Description: A visual editor for Haskell exists, but unfortunately, it is not very usable in practice. Since Haskell is a functional programming language (and hence has no control flow - loops, conditionals, etc), a visual editor can be very appropriate. The project aims to produce a visual editor particularly suited for list and datatype manipulation functions, and which handles refinement effectively, making it usable in Haskell software development.
    Requirements: Strong programming skills.

  • Title: Using Haskell as a Scripting Language for a Vector Graphics Editor
    Supervisor: Gordon Pace and Joseph Cordina
    Description: Various applications benefit from a scripting language, to enable the automation of repetitive tasks - one finds programmable macros in word processors, and in spreadsheets (eg MS Word and Excel using Visual Basic), in text editors (eg Emacs using Lisp), CAD software (eg AutoCAD using Lisp), etc.

    The aim of this project is to enhance an open-source vector-based graphics editor (eg XFig) with a Haskell based scripting language, enabling the user to script commands which draw, interact with the user, access the menus, etc.
    Requirements: Strong programming skills.

  • Title: Teaching System Architecture Using Haskell and Lava
    Supervisor: Gordon Pace
    Description: Lava is a hardware description language embedded in Haskell, allowing elegant descriptions of regular hardware systems. The student taking this FYP will use Lava and Haskell to create a pedagological suite of tools for computer science students to understand better, and experiment with the different layers in a computer system. A simple processor defined in Lava, will allow students to experiment with processor design. A small assembler (built as an embedded language in Haskell) will then allow the students to study the interaction between the machine and simple programs. A small operating system written in the assembly language will then abstract away the machine. A high level language compiler will then complete the suite. Various techniques for fast simulation and different approaches to understandable, concise descriptions of the different modules should be explored in this project.
    Requirements: Strong programming skills.

  • Title: Optimised Compilation of Mode Automata
    Supervisor: Gordon Pace
    Description: Modes are an alternative method of programming, whereby a programmer associates a particular piece of code with a particular mode (a sort of labelled state). The programmer then specifies mode transition conditions that when met will halt the currently running mode and will continue executing the code in another mode. In this FYP, you will be given a concrete language syntax for specifying modes and the corresponding actions within the modes and you will implement this language in Haskell (as an embedded language). The aim of this is to investigate the translation process from the higher level syntax to actual execution code. The next step (and most important) would be to investigate ways in which the compilation process can be optimised to generate efficient execution code. This step can be done within or outside of Haskell as you may see fit.
    Requirements: Strong programming skills.

  • Title: Strengthening C with Strong Types
    Supervisor: Gordon Pace
    Description: The C language has gained wide-spread use in both academic instutions and industry. The main reason is the flexibility and efficiency provided by this language. Functional Programmers commonly attribute the strength of the functional paradigm to the commonly associated strong type system and the availability of static type checking. In fact, functional programmers state that most bugs are a result of type errors (something that C is not very good at capturing).
    In this FYP, you will be building an extension to the C language that allows Haskell like data types to be defined in C. Additionally you will then be able to build a static type checker (and maybe also a type inference engine), that will guarantee proper type usage. Having a strong type system, you will also be able to enhance C to implement pattern matching on the types. To be able to execute this Strongly-Typed-C, you will build a pre-processor that will then translate the new syntax to traditional C code, that can get be compiled using off the shelf compilers, but still maintaining all the strengths of the original specification.
    Requirements: Strong programming skills in both C and a strongly typed language (ex Haskell).


Implementation of an SPDI Model Checker
Supervisor: Gordon Pace
Description: In [1,2], we have presented a new algorithm for model checking of SPDI Hybrid Systems. The new algorithm, as compared to the original presented in [3], and implemented in SPeeDI [4] offers various advantages, in that it enables standard model-checking optimisations to be applied. The aim of this project would be to implement the new algorithm (possibly by building over the Haskell libraries already built in SPeeDI), compare the results with those obtained in SPeeDI and investigate various optimisations to the algorithm.
Requirements: Strong in mathematics and an enthusiastic Haskell hacker.
References:
  • [1] Gordon J. Pace and Gerardo Schneider, University of Oslo, Model Checking Polygonal Differential Inclusions Using Invariance Kernels, in Verification and Model Checking and Abstract Interpretation (VMCAI 2004), LNCS, Venice, Italy, 2004.
  • [2] Gordon J. Pace, A New Breadth-First Search Algorithm for Deciding SPDI Reachability, Department of Computer Science and AI, University of Malta. Technical Report CSAI2003-01, 2003.
  • [3] Eugene Asarin, Gerardo Schneider, Sergio Yovine, On the decidability of the reachability problem for Planar Differential Inclusions, in HSCC'01, LNCS 2034, Springer-Verlag, 2001.
  • [4] Eugene Asarin, Gordon Pace, Gerardo Schneider, Sergio Yovine, SPeeDI - A Verification Tool for Polygonal Hybrid Systems, in Computer-Aided Verification (CAV 2002) published in LNCS 2404, Copenhagen, Denmark, 2002.

Implementation of Maltese in the Grammatical Framework
Supervisor: Gordon Pace and Joseph Cordina
Description: The Language Technology Group at Chalmers (part of Gothenburg University, Sweden) has embarked on a project that aims to implement automated natural language translation from and to all 23 official EU languages. One of the languages still pending implementation is the Maltese Language. The group has implemented INTERLINGUA, a language representation that is independent of any particular language, yet general enough to be able to encompass all grammatical rules of the above EU languages. To implement a concrete language, one creates a concrete syntax for a particular language and then defines a reversible mapping from this concrete syntax to the interlingua representation. Several languages have been implemented in this way, and through this procedure one gets for free the translation to and from all other implemented languages. The aim of this FYP is to implement a subset of the Maltese language using the GF, a software library used to define the concrete syntax and mapping explained above. As a test application, a mathematical exercise translator needs to be implemented (to be linked with WebALT). This translator may also be used by an industrial partner. More information on the EU languages project can be obtained from its website. The tutorial at this site is an excellent place to start from.
Requirements: Interest in Maltese and Natural Language Processing and an enthusiastic Haskell hacker.
References:
  • [1] A. Ranta, Grammatical Framework: A Type-Theoretical Grammar Formalism, The Journal of Functional Programming, vol. 14:2. 2004.
  • [2] Peter Ljunglof, Expressivity and Complexity of the Grammatical Framework, PhD Thesis, Chalmers Technical University, 2001.

Static Checking of Web-Related Programs
Supervisor: Gordon Pace and Guillermo A. Francia III
Description: Webpages today are normally generated using server side scripts that at runtime generate both html code and also code like Javascript which is then executed inside the client side browser. With so many layers and complexity, it is common for webpages to become susceptible to security flaws that are exploited once spotted.

Since hackers make use of well-known patterns within the code to administer attacks, the same approach can be taken by those who want to secure the webpage. Automated tools exist that are able to analyse the server side scripts and the generated code for the existence of these patterns.

Unfortunately there it is not easy to upgrade these tools to check for newly found patterns. This is normally done by painstakingly modifying the tools source code, which can lead to bugs within the checking tools!

The aim of this master's dissertation is to design a language that is able to describe patterns that represent security holes. These patterns should ideally be described in a way that is language independent, by symbolically describing language structures. This meta-language can be used to describe `bad' patterns, and used to analyse both webpages (say containing Javascript) or server side scripts (say written in PHP) for the patterns described in your language.

The language can be embedded in Haskell, to enable consise descriptions of regular patterns. This approach has the advantage of being able to easily describe new patterns. Additionally one can build a consistency checker, to ensure that different patterns do not contradict each other. This approach can be integrated in a web browser, where unsafe webpages are flagged, and on the server side where a server will stop the execution of 'unsafe' scripts.
References:
  • [1] Paul Hudak, Building Domain-Specific Embedded Languages, ACM Computing Surveys 28A(4), December 1996.
  • [2] Simon Peyton Jones (editor), Haskell 98 Language and Libraries: The Revised Report, available from www.haskell.org , December 2002.
  • [3] André Santos, Embedding a Firewall programming language into Haskell, SBLP'99 - III Simposio Brasileiro de Linguagens de Programacao, Porto Alegre, 1999.
  • [4] Hoglund and McGraw, Exploiting Software How to Break Code, Addison Wesley, 2004.
  • [5] Gallagher, Jeffries and Landauer, Hunting Security Bugs, Microsoft Press, 2006.

Web-based Penetration Testing
Supervisor: Gordon Pace and Guillermo A. Francia III
Description: In a webpage, a form is a two way communication between a server and the client. Passing malicious information through a form might be a way to hack into the server's data and computer. A hacker will usually start off analysing the vulnerabilities of a particular server by passing data through the form and seeing how the server responds. Since the server's scripts are not available to the hacker, he will make use of a number of well-known attack patterns. Often most programmers do not check for certain backdoors on the server scripts and thus someone may find ways to hack into the server's data.

The aim of this masters project, is to design an embedded language in Haskell that is able to effectively describe these attack patterns in a clear and compositional manner. Descriptions in the language will be used so that, given a form-based webpage, one will be able to replay the attack patterns on the webpage and analyse the results - a form of black box testing, since one gains information on the server's scripts to which one has no access to the sources. From this information, the security of the server scripts can be assessed. Additionally the attack patterns can be used to automatically generate test cases.

An extension can be built, to use a grey-box testing approach, where some information from the server scripts will be known to the testing tool. This information may include information such as server-script language used, web-server version and also information about some entry passwords.
References:
  • [1] Paul Hudak, Building Domain-Specific Embedded Languages, ACM Computing Surveys 28A(4), December 1996.
  • [2] Simon Peyton Jones (editor), Haskell 98 Language and Libraries: The Revised Report, available from www.haskell.org , December 2002.
  • [3] André Santos, Embedding a Firewall programming language into Haskell, SBLP'99 - III Simposio Brasileiro de Linguagens de Programacao, Porto Alegre, 1999.
  • [4] Hoglund and McGraw, Exploiting Software How to Break Code, Addison Wesley, 2004.
  • [5] Gallagher, Jeffries and Landauer, Hunting Security Bugs, Microsoft Press, 2006.

Embedded Languages
Embedded languages have been developed in the programming language research community, in which a programming language is embedded inside another language (called the host language) as a data structure or collection of methods. The host language can then be used to generate regular instances of the embedded language, simulate programs, compile them, etc.
  • Title: Embedding Floyd-Hoare Reasoning About Programs
    Supervisor: Gordon Pace and Joseph Cordina
    Description: Floyd-Hoare logic gives an easy way of reasoning about imperative programs. Given a simple imperative programming language embedded in a functional language, it would be possible to automatically try to generate Floyd-Hoare properties and simplify them, possibly through interaction with the user or external tools. The aim of the project would be that of assessing the use of embedded languages in reasoning about programming languages.
    Requirements: Strong in discrete mathematics.


Verification, Validation and Model Checking
Verification is the use of mathematical tools to prove the correctness of a system. Model Checking is used for such techniques which verify other systems automatically (ie via the use of software).

  • Title: Model Checking Infinite Families of Parallel Systems
    Supervisor: Joseph Cordina and Gordon Pace
    Description: Regular parallel systems can be defined in terms of a simple set of rules. For example, a tree structure can be expressed as the (infinite) family: P ::= Base | P || Node || P (where || is parallel composition, Base is the node appearing at the leaves of the tree, and the Node connects the subnodes in some way). Using structural induction, it is possible to reduce the verification of this infinite set of systems into proofs of finite systems, by proving that (i) Base satisfies the property, and (ii) if P and Q satisfy the property, then so does P || Node || Q. The techniques are very similar to the ones described in the previous proposal. The aim of the project would be to identify a class of interesting regular systems and verify such a family using a standard finite state model checker.
    Requirements: Very strong in discrete mathematics, good systems background.

  • Title: Automata Specification for QuickCheck
    Supervisor: Gordon Pace and Joseph Cordina
    Description: QuickCheck (check this website) is an automatic testing tool for Haskell programs, which automatically generates random inputs to test functions against a given specification. This technique works very well with most programs, but in certain cases, where the order of execution of certain functions can make or break a specification, it helps to augment the approach also with a specification of how certain functions are called. For example, one can test that if one pushes some data a number of times on a stack, one can then pop data that many times without causing errors. The aim of this project is to build a system above QuickCheck, which enables the user to specify how functions are composed together using an automaton or regular expression-like syntax to make the use of QuickCheck easier in such cases.
    Requirements: Interest in Haskell and testing.


Others
  • Title: A Maltese Parser using Context-Sensitive Parser Combinators
    Supervisor: Gordon Pace
    Description: Combinator-based programming provides an elegant and compositional way of constructing a program. Various parser combinators have been proposed for Haskell. In particular, in [1], we have contructed a set of parser combinators which allow reference to the context - hence making them particularly useful for natural language parsing, where local transformations can take place (eg the indefinite article a or an in English depends on the beginning of the next word) and sentence level context (such as matching of gender and tense across a sentence). The transparent use of non-determinism in these parser combinators make such descriptions succint and easy to understand. In [1], these combinators were used to parse simple sentences in Maltese. The aim of this project is to apply these combinators to a larger subset of Maltese - possibly constrained to a particular domain (such as legal texts), enabling parsing and analysis of Maltese texts. One possible direction this project can take is also the automatic generation of Maltese text based on an internal logic representation using the same (or similar) combinators.
    Requirements: The student taking this project is expected to have a strong interest in Maltese and natural language processing and also be an enthusiastic Haskell hacker.
    References:
    • [1] Gordon J. Pace, Monadic Compositional Parsing with Context Using Maltese as a Case Study, Computer Science Annual Workshop 2004, Department of Computer Science and AI, University of Malta, 2004.