Diff of /metadata/metadata [4b7998] .. [f01853]  Maximize  Restore

  Switch to side-by-side view

--- a/metadata/metadata
+++ b/metadata/metadata
@@ -511,6 +511,34 @@
 topic = Computer Science/Programming Languages/Logics, Computer Science/Security
 abstract = We present interpretations of type systems for secure information flow in Hoare logic, complementing previous encodings in relational program logics. We first treat the imperative language IMP, extended by a simple procedure call mechanism. For this language we consider base-line non-interference in the style of Volpano et al. and the flow-sensitive type system by Hunt and Sands. In both cases, we show how typing derivations may be used to automatically generate proofs in the program logic that certify the absence of illicit flows. We then add instructions for object creation and manipulation, and derive appropriate proof rules for base-line non-interference. As a consequence of our work, standard verification technology may be used for verifying that a concrete program satisfies the non-interference property.<br><br>The present proof development represents an update of the formalisation underlying our paper [CSF 2007] and is intended to resolve any ambiguities that may be present in the paper. 
+title = A Definitional Encoding of TLA in Isabelle/HOL
+author = Gudmund Grov <http://homepages.inf.ed.ac.uk/ggrov>, Stephan Merz <http://www.loria.fr/~merz>
+date = 2011-11-19
+topic = Computer Science/Programming Languages/Logics
+abstract = We mechanise the logic TLA*
+ <a href="http://www.springerlink.com/content/ax3qk557qkdyt7n6/">[Merz 1999]</a>,
+ an extension of Lamport's  Temporal Logic of Actions (TLA)
+ <a href="http://dl.acm.org/citation.cfm?doid=177492.177726">[Lamport 1994]</a>
+ for specifying and reasoning
+ about concurrent and reactive systems. Aiming at a framework for mechanising]  the verification of TLA (or TLA*) specifications, this contribution reuses
+ some elements from a previous axiomatic encoding of TLA in Isabelle/HOL
+ by the second author [Merz 1998], which has been part of the Isabelle
+ distribution. In contrast to that previous work, we give here a shallow,
+ definitional embedding, with the following highlights:
+ <ul>
+ <li>a theory of infinite sequences, including a formalisation of the concepts of stuttering invariance central to TLA and TLA*;
+ <li>a definition of the semantics of TLA*, which extends TLA by a mutually-recursive definition of formulas and pre-formulas, generalising TLA action formulas;
+ <li>a substantial set of derived proof rules, including the TLA* axioms and Lamport's proof rules for system verification;
+ <li>a set of examples illustrating the usage of Isabelle/TLA* for reasoning about systems.
+ <ul>
+ Note that this work is unrelated to the ongoing development of a proof system
+ for the specification language TLA+, which includes an encoding of TLA+ as a
+ new Isabelle object logic <a href="http://www.springerlink.com/content/354026160p14j175/">[Chaudhuri et al 2010]</a>.
+ <p>
+ A previous version of this embedding has been used heavily in the work
+ described in the PhD thesis [Grov 2009].
 title = Compiling Exceptions Correctly
 author = Tobias Nipkow <http://www.in.tum.de/~nipkow/>

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

No, thanks