A Hoare logic for linear systems

Rob Arthan, Ursula Martin, Paulo Oliva

Research output: Contribution to journalArticlepeer-review


We consider reasoning about linear systems expressed as block diagrams that give a graphical representation of a system of differential equations or recurrence equations. We use the notion of additive relation borrowed from homological algebra to give a convenient framework in which all diagrams have a semantic value. We give a sound system of Hoare-style rules for the block diagram constructors that singles out a tractable subset of the block diagram language in which all diagrams represent total functions. We show these rules in action on some simple examples from a variety of applications domains.
Original languageEnglish
Pages (from-to)345-363
Number of pages19
JournalFormal Aspects of Computing
Issue number3
Early online date11 May 2011
Publication statusPublished - May 2013

Fingerprint Dive into the research topics of 'A Hoare logic for linear systems'. Together they form a unique fingerprint.

Cite this