Abstract. CIRC is an automated circular coinductive prover implemented as an extension of Maude. The circular coinductive technique that forms the core of CIRC is discussed, togeth...
Specification-based testing is a particular case of black-box testing, which consists in deriving test cases from an analysis of a formal specification. We present in this paper an...
Goldblatt and Thomason’s theorem on modally definable classes of Kripke frames and Venema’s theorem on modally definable classes of Kripke models are generalised to coalgebra...
Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One can prove a coinduction step s...
Adhesive categories are a class of categories in which pushouts along monos are well-behaved with respect to pullbacks. Recently it has been shown that any topos is adhesive. Many ...
Peter T. Johnstone, Stephen Lack, Pawel Sobocinski
Much current work on modelling and verifying microprocessors can accommodate pipelined and superscalar processors. However, superscalar and pipelined processors are no longer state...