- Thursday 13th March 2008 [3pm]
- Dynamic Analysis Overview and a Proposed Verification Tool for Temporal Properties in Security Critical Software
(Christian Colombo)
Abstract:
The need for correct software is increasing as computers are proliferating in every aspect of our lives. Dynamic analysis is a possible way of increasing the reliability of software by introducing a monitoring and verification mechanism over and above a computer system, so that if under some unprecedented circumstance, any of its specifications are violated, an alarm will be raised. This paper gives an overview of the literature in the subject and also puts forward a proposal of further research and investigation which seems to be very promising.
- Thursday 28th February 2008 [12pm]
- LARVA - Logical Automata for Runtime Verification and Analysis (Christian Colombo)
Abstract:
Robustness and reliability are key factors in the success of the deployment of security-critical systems. Testing, fails to address these concerns adequately since not all possible execution paths are covered. On the other hand, verification - the analysis of all execution paths - is usually unfeasible due to the large state space of such systems. Runtime-verification addresses the issue by enabling formal verification of the system during its execution.
An adequate logic and language to express typical security properties is a prerequisite to enable runtime verification. In this talk, we will present LARVA, a runtime verification platform for runtime verification of critical systems. We will focus on the logic and property specification language, discussing issues of expressivity, automatic weaving into the monitored system, and the overhead induced. At the end, the presentation will take the form of a discussion to gather feedback about the language from potential end users currently involved in large industrial projects.
- Friday 22nd February 2008 [2:30pm]
- Meta Functional Languages for Hardware Design (Christian Tabone)
Abstract:
As innovative circuit designs increase in size and complexity, hardware description techniques have been trying to adopt some of the successful features offered by software languages. In this paper, we investigate how different hardware description languages implement levels of abstraction over the hardware designs, and we examine how improvements have lead to features like parameterised circuits and generic descriptions, that enable users to efficiently model and reason about large regular-shaped structures and connection patterns. Nonetheless, the ability to include the non-functional properties of circuits is still an open issue. Lately, proposed solutions are looking into meta-functional languages. We examine how hardware description languages can benefit from the capabilities of meta-functional languages, which are able to reason about, and transform the circuit generators as data objects, thus providing a means to access both the functional and non-functional aspects of the generated circuits.
- Friday 26th October 2007 [2pm]
- Verification of refactorings in Isabelle/HOL (Nikolai Sultana)
Abstract:
Refactorings are source-to-source behaviour-preserving program
transformations that are used for improving program structure.
Programmers refactor code to adapt it when new functionality is
added or when the code is being repaired -- refactoring serves
to keep the code "clean" and more maintainable. Refactoring
can also be used as an exploratory technique for understanding
source code.
The process of refactoring has been automated through the
implementation of tools. It is desirable that these
implementations are free from bugs otherwise this might lead to
unspecified behaviour when refactored code is executed.
We will describe the verification of refactorings for untyped
and typed lambda-calculi. This verification has been done using
the proof assistant Isabelle/HOL. We will also discuss technical
difficulties encountered, alternative methods considered and
other approaches for proving refactorings correct.
|
|