Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
dd8e0cdca49e
Commit
770e364e
authored
Jan 12, 2021
by
Manuel Eberl
Browse files
sitegen for CSP_RefTK
parent
626c957d2647
Changes
7
Expand all
Hide whitespace changes
Inline
Side-by-side
metadata/metadata
View file @
dd8e0cdc
...
...
@@ -9995,3 +9995,28 @@ abstract =
technique we can effectively harness theorem provers, model finders
and 'hammers' for reasoning with quantified non-classical
logics.
[CSP_RefTK]
title = The HOL-CSP Refinement Toolkit
author = Safouan Taha <mailto:safouan.taha@lri.fr>, Burkhart Wolff <https://www.lri.fr/~wolff/>, Lina Ye <mailto:lina.ye@lri.fr>
topic = Computer science/Concurrency/Process calculi, Computer science/Semantics
date = 2020-11-19
notify = wolff@lri.fr
abstract =
We use a formal development for CSP, called HOL-CSP2.0, to analyse a
family of refinement notions, comprising classic and new ones. This
analysis enables to derive a number of properties that allow to deepen
the understanding of these notions, in particular with respect to
specification decomposition principles for the case of infinite sets
of events. The established relations between the refinement relations
help to clarify some obscure points in the CSP literature, but also
provide a weapon for shorter refinement proofs. Furthermore, we
provide a framework for state-normalisation allowing to formally
reason on parameterised process architectures. As a result, we have a
modern environment for formal proofs of concurrent systems that allow
for the combination of general infinite processes with locally finite
ones in a logically safe way. We demonstrate these
verification-techniques for classical, generalised examples: The
CopyBuffer for arbitrary data and the Dijkstra's Dining
Philosopher Problem of arbitrary size.
web/entries/CSP_RefTK.html
0 → 100644
View file @
dd8e0cdc
<!DOCTYPE html>
<html
lang=
"en"
>
<head>
<meta
charset=
"utf-8"
>
<title>
The HOL-CSP Refinement Toolkit - Archive of Formal Proofs
</title>
<link
rel=
"stylesheet"
type=
"text/css"
href=
"../front.css"
>
<link
rel=
"icon"
href=
"../images/favicon.ico"
type=
"image/icon"
>
<link
rel=
"alternate"
type=
"application/rss+xml"
title=
"RSS"
href=
"../rss.xml"
>
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax
=
{
tex
:
{
inlineMath
:
[[
'
$
'
,
'
$
'
],
[
'
\\
(
'
,
'
\\
)
'
]]
},
processEscapes
:
true
,
svg
:
{
fontCache
:
'
global
'
}
};
</script>
<script
id=
"MathJax-script"
async
src=
"../components/mathjax/es5/tex-mml-chtml.js"
></script>
</head>
<body
class=
"mathjax_ignore"
>
<table
width=
"100%"
>
<tbody>
<tr>
<!-- Navigation -->
<td
width=
"20%"
align=
"center"
valign=
"top"
>
<p>
</p>
<a
href=
"https://www.isa-afp.org/"
>
<img
src=
"../images/isabelle.png"
width=
"100"
height=
"88"
border=
0
>
</a>
<p>
</p>
<p>
</p>
<table
class=
"nav"
width=
"80%"
>
<tr>
<td
class=
"nav"
width=
"100%"
><a
href=
"../index.html"
>
Home
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../about.html"
>
About
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../submitting.html"
>
Submission
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../updating.html"
>
Updating Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../using.html"
>
Using Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../search.html"
>
Search
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../statistics.html"
>
Statistics
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../topics.html"
>
Index
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../download.html"
>
Download
</a></td>
</tr>
</table>
<p>
</p>
<p>
</p>
</td>
<!-- Content -->
<td
width=
"80%"
valign=
"top"
>
<div
align=
"center"
>
<p>
</p>
<h1>
<font
class=
"first"
>
T
</font>
he
<font
class=
"first"
>
H
</font>
OL-CSP
<font
class=
"first"
>
R
</font>
efinement
<font
class=
"first"
>
T
</font>
oolkit
</h1>
<p>
</p>
<table
width=
"80%"
class=
"data"
>
<tbody>
<tr>
<td
class=
"datahead"
width=
"20%"
>
Title:
</td>
<td
class=
"data"
width=
"80%"
>
The HOL-CSP Refinement Toolkit
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Authors:
</td>
<td
class=
"data"
>
Safouan Taha (safouan /dot/ taha /at/ lri /dot/ fr),
<a
href=
"https://www.lri.fr/~wolff/"
>
Burkhart Wolff
</a>
and
Lina Ye (lina /dot/ ye /at/ lri /dot/ fr)
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Submission date:
</td>
<td
class=
"data"
>
2020-11-19
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
Abstract:
</td>
<td
class=
"abstract mathjax_process"
>
We use a formal development for CSP, called HOL-CSP2.0, to analyse a
family of refinement notions, comprising classic and new ones. This
analysis enables to derive a number of properties that allow to deepen
the understanding of these notions, in particular with respect to
specification decomposition principles for the case of infinite sets
of events. The established relations between the refinement relations
help to clarify some obscure points in the CSP literature, but also
provide a weapon for shorter refinement proofs. Furthermore, we
provide a framework for state-normalisation allowing to formally
reason on parameterised process architectures. As a result, we have a
modern environment for formal proofs of concurrent systems that allow
for the combination of general infinite processes with locally finite
ones in a logically safe way. We demonstrate these
verification-techniques for classical, generalised examples: The
CopyBuffer for arbitrary data and the Dijkstra's Dining
Philosopher Problem of arbitrary size.
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
BibTeX:
</td>
<td
class=
"formatted"
>
<pre>
@article{CSP_RefTK-AFP,
author = {Safouan Taha and Burkhart Wolff and Lina Ye},
title = {The HOL-CSP Refinement Toolkit},
journal = {Archive of Formal Proofs},
month = nov,
year = 2020,
note = {\url{https://isa-afp.org/entries/CSP_RefTK.html},
Formal proof development},
ISSN = {2150-914x},
}
</pre>
</td>
</tr>
<tr><td
class=
"datahead"
>
License:
</td>
<td
class=
"data"
><a
href=
"http://isa-afp.org/LICENSE"
>
BSD License
</a></td></tr>
<tr><td
class=
"datahead"
>
Depends on:
</td>
<td
class=
"data"
><a
href=
"HOL-CSP.html"
>
HOL-CSP
</a>
</td></tr>
</tbody>
</table>
<p></p>
<table
class=
"links"
>
<tbody>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/CSP_RefTK/outline.pdf"
>
Proof outline
</a><br>
<a
href=
"../browser_info/current/AFP/CSP_RefTK/document.pdf"
>
Proof document
</a>
</td>
</tr>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/CSP_RefTK/index.html"
>
Browse theories
</a>
</td></tr>
<tr>
<td
class=
"links"
>
<a
href=
"../release/afp-CSP_RefTK-current.tar.gz"
>
Download this entry
</a>
</td>
</tr>
<tr><td
class=
"links"
>
Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script
src=
"../jquery.min.js"
></script>
<script
src=
"../script.js"
></script>
</body>
</html>
\ No newline at end of file
web/entries/HOL-CSP.html
View file @
dd8e0cdc
...
...
@@ -148,7 +148,9 @@ in Isar and is substantially shorter but more complete.</td>
<tr><td
class=
"datahead"
>
Used by:
</td>
<td
class=
"data"
><a
href=
"CSP_RefTK.html"
>
CSP_RefTK
</a>
</td></tr>
</tbody>
...
...
web/index.html
View file @
dd8e0cdc
...
...
@@ -130,6 +130,16 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
Hanna Lachnitt
and Yijun He
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-11-19:
<a
href=
"entries/CSP_RefTK.html"
>
The HOL-CSP Refinement Toolkit
</a>
<br>
Authors:
Safouan Taha,
<a
href=
"https://www.lri.fr/~wolff/"
>
Burkhart Wolff
</a>
and Lina Ye
</td>
</tr>
<tr>
<td
class=
"entry"
>
...
...
web/rss.xml
View file @
dd8e0cdc
...
...
@@ -88,6 +88,30 @@ matrix representation for quantum circuits, successfully formalising
the no-cloning theorem, quantum teleportation, Deutsch
'
s
algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner
'
s
Dilemma.
</description>
</item>
<item>
<title>
The HOL-CSP Refinement Toolkit
</title>
<link>
https://www.isa-afp.org/entries/CSP_RefTK.html
</link>
<guid>
https://www.isa-afp.org/entries/CSP_RefTK.html
</guid>
<dc:creator>
Safouan Taha, Burkhart Wolff, Lina Ye
</dc:creator>
<pubDate>
19 Nov 2020 00:00:00 +0000
</pubDate>
<description>
We use a formal development for CSP, called HOL-CSP2.0, to analyse a
family of refinement notions, comprising classic and new ones. This
analysis enables to derive a number of properties that allow to deepen
the understanding of these notions, in particular with respect to
specification decomposition principles for the case of infinite sets
of events. The established relations between the refinement relations
help to clarify some obscure points in the CSP literature, but also
provide a weapon for shorter refinement proofs. Furthermore, we
provide a framework for state-normalisation allowing to formally
reason on parameterised process architectures. As a result, we have a
modern environment for formal proofs of concurrent systems that allow
for the combination of general infinite processes with locally finite
ones in a logically safe way. We demonstrate these
verification-techniques for classical, generalised examples: The
CopyBuffer for arbitrary data and the Dijkstra
'
s Dining
Philosopher Problem of arbitrary size.
</description>
</item>
<item>
<title>
Verified SAT-Based AI Planning
</title>
...
...
@@ -578,19 +602,5 @@ AFP entries. This permits to reuse results from both developments and
it is done by means of the lifting and transfer package together with
the use of local type definitions.
</description>
</item>
<item>
<title>
The Nash-Williams Partition Theorem
</title>
<link>
https://www.isa-afp.org/entries/Nash_Williams.html
</link>
<guid>
https://www.isa-afp.org/entries/Nash_Williams.html
</guid>
<dc:creator>
Lawrence C. Paulson
</dc:creator>
<pubDate>
16 May 2020 00:00:00 +0000
</pubDate>
<description>
In 1965, Nash-Williams discovered a generalisation of the infinite
form of Ramsey
'
s theorem. Where the latter concerns infinite sets
of n-element sets for some fixed n, the Nash-Williams theorem concerns
infinite sets of finite sets (or lists) subject to a “no initial
segment” condition. The present formalisation follows a
monograph on Ramsey Spaces by Todorčević.
</description>
</item>
</channel>
</rss>
web/statistics.html
View file @
dd8e0cdc
This diff is collapsed.
Click to expand it.
web/topics.html
View file @
dd8e0cdc
...
...
@@ -234,6 +234,7 @@
<a
href=
"entries/Noninterference_Concurrent_Composition.html"
>
Noninterference_Concurrent_Composition
</a>
<a
href=
"entries/Modal_Logics_for_NTS.html"
>
Modal_Logics_for_NTS
</a>
<a
href=
"entries/HOL-CSP.html"
>
HOL-CSP
</a>
<a
href=
"entries/CSP_RefTK.html"
>
CSP_RefTK
</a>
</div>
<h3>
Data structures
</h3>
<div
class=
"list"
>
...
...
@@ -489,6 +490,7 @@
<a
href=
"entries/QHLProver.html"
>
QHLProver
</a>
<a
href=
"entries/TESL_Language.html"
>
TESL_Language
</a>
<a
href=
"entries/Isabelle_C.html"
>
Isabelle_C
</a>
<a
href=
"entries/CSP_RefTK.html"
>
CSP_RefTK
</a>
</div>
<h3>
System description languages
</h3>
<div
class=
"list"
>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment