SmallCheck: Another Lightweight Tool for Testing Functional Properties
Colin Runciman (York)
If there is any case in which a program fails, there is almost always a simple one, and the simplest cases are the easiest to investigate. Such observations motivate the development of SmallCheck, a combinator library for property-based testing in the functional language Haskell.
SmallCheck is similar to a widely-used tool called QuickCheck: it uses the same idea of type-based generators for test data; the way testable properties are expressed follows the QuickCheck approach; SmallCheck also tests whether properties hold for finite fully-defined values at specific types, and reports counter-examples. The big difference is that instead of using a sample of randomly generated values, SmallCheck tests properties for all the finitely many values up to some size, progressively increasing the size used.
The talk will include illustrative examples of how SmallCheck can be used. It will also explore some design and implementation issues, and point out some remaining challenges.
Epistemic Logics for Time and Space Bounded Reasoning
Natasha Alechina (Nottingham)
Joint work with Brian Logan and Mark Jago from the University of Nottingham and Piergiorgio Bertoli, Chiara Ghidini and Luciano Serafini from ITC-irst, Trento, and Thomas Agotnes from the University of Bergen.
In standard epistemic logics, an agent's beliefs are modelled as closed under logical consequence. This becomes a problem if we are interested in the evolution of beliefs of a rational agent which requires time and memory to derive consequences of its beliefs. For example, we may be interested in expressing and verifying properties like `given its current beliefs and its memory size, the agent will/will not believe A in the next n time steps', where A may be a consequence of the agent's beliefs. The basic idea of our approach is as follows. The reasoning agent is modelled as a state transition system; each state is a finite set of formulas (agent's beliefs); the maximal size of this set is determined by the agent's memory size. Transitions between states correspond to applications of the agent's inference rules. The language of temporal epistemic logic can be interpreted in such structures in a straightforward way. Several interesting directions for research arise, for example:
- completeness and decidability of epistemic logics for particular kinds of reasoners (determined by their inference rules);
- expressive power: adding epistemic operators which allow us to express properties like `the agent has memory of size n' and `the memory is not full';
- automatic verification: we are using MBP (model-based planner, developed in Trento) to verify memory requirements for a classical reasoner and a rule-based reasoner.
The Star and Beyond: Algebraic Notions of Termination and Divergence
Georg Struth (Sheffield)
Idempotent semirings extended by notions of finite iteration (the star) and infinite iteration (the omega) are foundational structures in computing science. They are expressive enough to cover a wide range of applications; they are simple enough for first-order equational reasoning supported by strong decision procedures and for admitting a rich model class. This talk surveys extensions of these algebras by Jónsson-Tarski-style modalities, some properties of the resulting modal semirings and some models. It discusses applications of modal semirings in modelling the terminating and infinite behaviour of transition systems. It reports on proof-automation experiments to demonstrate their potential in formal software development.
Lecture Theatre SB-LT01
Sir Henry Stephenson Building
Please use the following links to find