The University of Adelaide
You are here
Text size: S | M | L
Printer Friendly Version
April 2019

Search the School of Mathematical Sciences

Find in People Courses Events News Publications

Events matching "Software and protocol verification using Alloy"

Modelling of the Human Skin Equivalent
15:10 Fri 26 Mar, 2010 :: Napier 102 :: Prof Graeme Pettet :: Queensland University of Technology

A brief overview will be given of the development of a so called Human Skin Equivalent Construct. This laboratory grown construct can be used for studying growth, response and the repair of human skin subjected to wounding and/or treatment under strictly regulated conditions. Details will also be provided of a series of mathematical models we have developed that describe the dynamics of the Human Skin Equivalent Construct, which can be used to assist in the development of the experimental protocol, and to provide insight into the fundamental processes at play in the growth and development of the epidermis in both healthy and diseased states.
Permeability of heterogeneous porous media - experiments, mathematics and computations
15:10 Fri 27 May, 2011 :: B.21 Ingkarni Wardli :: Prof Patrick Selvadurai :: Department of Civil Engineering and Applied Mechanics, McGill University

Permeability is a key parameter important to a variety of applications in geological engineering and in the environmental geosciences. The conventional definition of Darcy flow enables the estimation of permeability at different levels of detail. This lecture will focus on the measurement of surface permeability characteristics of a large cuboidal block of Indiana Limestone, using a surface permeameter. The paper discusses the theoretical developments, the solution of the resulting triple integral equations and associated computational treatments that enable the mapping of the near surface permeability of the cuboidal region. This data combined with a kriging procedure is used to develop results for the permeability distribution at the interior of the cuboidal region. Upon verification of the absence of dominant pathways for fluid flow through the cuboidal region, estimates are obtained for the "Effective Permeability" of the cuboid using estimates proposed by Wiener, Landau and Lifschitz, King, Matheron, Journel et al., Dagan and others. The results of these estimates are compared with the geometric mean, derived form the computational estimates.
Textbooks go interactive but are they any better?
12:10 Mon 15 Aug, 2011 :: 5.57 Ingkarni Wardli :: Mr Patrick Korbel :: University of Adelaide

Textbooks remain a central part of mathematics lessons in secondary schools. However, while textbooks are still formatted in the traditional way, they are including increasingly more sophisticated software packages to assist teachers and students. I will be demonstrating the different software packages available to students included with two South Australian textbooks. I will talk about how these new features fit into the current classroom environment and some of their potential positives and negatives. I would also like to encourage people to share their own experiences with textbooks, especially if they were used in a novel way or you have experience of mathematics classes in another country.
AD Model Builder and the estimation of lobster abundance
12:10 Mon 22 Oct, 2012 :: B.21 Ingkarni Wardli :: Mr John Feenstra :: University of Adelaide

Determining how many millions of lobsters reside in our waters and how it changes over time is a central aim of lobster stock assessment. ADMB is powerful optimisation software to model and solve complex non-linear problems using automatic differentiation and plays a major role in SA and worldwide in fisheries stock assessment analyses. In this talk I will provide a brief description of an example modelling problem, key features and use of ADMB.
A model for the BitCoin block chain that takes propagation delays into account
15:10 Fri 28 Mar, 2014 :: B.21 Ingkarni Wardli :: Professor Peter Taylor :: The University of Melbourne

Unlike cash transactions, most electronic transactions require the presence of a trusted authority to verify that the payer has sufficient funding to be able to make the transaction and to adjust the account balances of the payer and payee. In recent years BitCoin has been proposed as an "electronic equivalent of cash". The general idea is that transactions are verified in a coded form in a block chain, which is maintained by the community of participants. Problems can arise when the block chain splits: that is different participants have different versions of the block chain, something which can happen only when there are propagation delays, at least if all participants are behaving according to the protocol. In this talk I shall present a preliminary model for the splitting behaviour of the block chain. I shall then go on to perform a similar analysis for a situation where a group of participants has adopted a recently-proposed strategy for gaining a greater advantage from BitCoin processing than its combined computer power should be able to control.
Software and protocol verification using Alloy
12:10 Mon 25 Aug, 2014 :: B.19 Ingkarni Wardli :: Dinesha Ranathunga :: University of Adelaide

Reliable software isn't achieved by trial and error. It requires tools to support verification. Alloy is a tool based on set theory that allows expression of a logic-based model of software or a protocol, and hence allows checking of this model. In this talk, I will cover its key concepts, language syntax and analysis features.
Modelling Coverage in RNA Sequencing
09:00 Mon 9 Nov, 2015 :: Ingkarni Wardli 5.57 :: Arndt von Haeseler :: Max F Perutz Laboratories, University of Vienna

RNA sequencing (RNA-seq) is the method of choice for measuring the expression of RNAs in a cell population. In an RNA-seq experiment, sequencing the full length of larger RNA molecules requires fragmentation into smaller pieces to be compatible with limited read lengths of most deep-sequencing technologies. Unfortunately, the issue of non-uniform coverage across a genomic feature has been a concern in RNA-seq and is attributed to preferences for certain fragments in steps of library preparation and sequencing. However, the disparity between the observed non-uniformity of read coverage in RNA-seq data and the assumption of expected uniformity elicits a query on the read coverage profile one should expect across a transcript, if there are no biases in the sequencing protocol. We propose a simple model of unbiased fragmentation where we find that the expected coverage profile is not uniform and, in fact, depends on the ratio of fragment length to transcript length. To compare the non-uniformity proposed by our model with experimental data, we extended this simple model to incorporate empirical attributes matching that of the sequenced transcript in an RNA-seq experiment. In addition, we imposed an experimentally derived distribution on the frequency at which fragment lengths occur.

We used this model to compare our theoretical prediction with experimental data and with the uniform coverage model. If time permits, we will also discuss a potential application of our model.
Interactive theorem proving for mathematicians
15:10 Fri 5 Oct, 2018 :: Napier 208 :: A/Prof Scott Morrison :: Australian National University

Mathematicians use computers to write their proofs (LaTeX), and to do their calculations (Sage, Mathematica, Maple, Matlab, etc, as well as custom code for simulations or searches). However today we rarely use computers to help us to construct and understand proofs. There is a long tradition in computer science of interactive and automatic theorem proving; particularly today these are important tools in engineering correct software, as well as in optimisation and compilation. There have been some notable examples of formalisation of modern mathematics (e.g. the odd order theorem, the Kepler conjecture, and the four-colour theorem). Even in these cases, huge engineering efforts were required to translate the mathematics to a form a computer could understand. Moreover, in most areas of research there is a huge gap between the interests of human mathematicians and the abilities of computer provers. Nevertheless, I think it's time for mathematicians to start getting interested in interactive theorem provers! It's now possible to write proofs, and write tools that help write proofs, in languages which are expressive enough to encompass most of modern mathematics, and ergonomic enough to use for general purpose programming. I'll give an informal introduction to dependent type theory (the logical foundation of many modern theorem provers), some examples of doing mathematics in such a system, and my experiences working with mathematics students in these systems.

Advanced search options

You may be able to improve your search results by using the following syntax:

QueryMatches the following
Asymptotic EquationAnything with "Asymptotic" or "Equation".
+Asymptotic +EquationAnything with "Asymptotic" and "Equation".
+Stokes -"Navier-Stokes"Anything containing "Stokes" but not "Navier-Stokes".
Dynam*Anything containing "Dynamic", "Dynamical", "Dynamicist" etc.