Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(4)
hoare logic
Linear Dynamical System
Separation Logic
Symmetric Monoidal Categories
Subscribe
Academic
Publications
Hoare Logic in the Abstract
Hoare Logic in the Abstract,10.1007/11874683_33,Ursula Martin,Erik A. Mathiesen,Paulo Oliva
Edit
Hoare Logic in the Abstract
(
Citations: 1
)
BibTex

RIS

RefWorks
Download
Ursula Martin
,
Erik A. Mathiesen
,
Paulo Oliva
We present an abstraction of
Hoare logic
to traced symmetric monoidal categories, a very general framework for the theory of systems. We first identify a particular class of functors � which we call �verification functors� � between traced
symmetric monoidal categories
and subcategories of (the category of preordered sets and monotone mappings). We then give an abstract definition of Hoare triples, parametrised by a verification functor, and prove a single soundness and completeness theorem for such triples. In the particular case of the traced symmetric
monoidal category
of while programs we get back Hoare�s original rules. We discuss how our framework handles extensions of the
Hoare logic
for while programs, e.g. the extension with pointer manipulations via separation logic. Finally, we give an example of how our theory can be used in the development of new Hoare logics: we present a new sound and complete set of Hoarelogiclike rules for the verification of linear dynamical systems, modelled via stream circuits.
Conference:
Computer Science Logic  CSL
, vol. 4207, pp. 501515, 2006
DOI:
10.1007/11874683_33
ISBN:
9783540454588
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
dx.doi.org
)
(
www.informatik.unitrier.de
)
More »
Citation Context
(1)
...There are theoretical indications that the FloydHoare approach applies to a very wide class of systems indeed [
9
]...
...Some experimentation has begun in applying the approach of the present paper to other systems (including one of the two main general types identified in [
9
]) with continuous systems as a goal...
R. D. Arthan
.
A Verified Formal Model of a VC Generator
References
(20)
Specification Structures and PropositionsasTypes for Concurrency
(
Citations: 22
)
Samson Abramsky
,
Simon J. Gay
,
Rajagopal Nagarajan
Conference:
Banff Higher Order Workshop
, pp. 540, 1995
Ten Years of Hoare's Logic: A Survey—Part I
(
Citations: 225
)
Krzysztof R. Apt
Journal:
ACM Transactions on Programming Languages and Systems  TOPLAS
, vol. 3, no. 4, pp. 431483, 1981
Feedback and Generalized Logic
(
Citations: 21
)
E. S. Bainbridge
Journal:
Information and Computation/information and Control  IANDC
, vol. 31, no. 1, pp. 7596, 1976
A logical analysis of aliasing in imperative higherorder functions
(
Citations: 31
)
Martin Berger
,
Kohei Honda
,
Nobuko Yoshida
Journal:
Sigplan Notices  SIGPLAN
, vol. 40, no. 9, pp. 280293, 2005
The Underlying Logic of Hoare Logic
(
Citations: 10
)
Andreas Blass
,
Yuri Gurevich
Journal:
Bulletin of The European Association for Theoretical Computer Science  EATCS
, 2001
Sort by:
Citations
(1)
A Verified Formal Model of a VC Generator
R. D. Arthan
Conference:
Annual Software Engineering Workshop  SEW
, pp. 263271, 2006