All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Page 1

Displaying 1 – 6 of 6

Showing per page

Taclets: a new paradigm for constructing interactive theorem provers.

Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, Steffen Schlager (2004)

RACSAM

Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules...

The Formalization of Decision-Free Petri Net

Pratima K. Shah, Pauline N. Kawamoto, Mariusz Giero (2014)

Formalized Mathematics

In this article we formalize the definition of Decision-Free Petri Net (DFPN) presented in [19]. Then we formalize the concept of directed path and directed circuit nets in Petri nets to prove properties of DFPN. We also present the definition of firing transitions and transition sequences with natural numbers marking that always check whether transition is enabled or not and after firing it only removes the available tokens (i.e., it does not remove from zero number of tokens). At the end of this...

Thread algebra for noninterference

Thuy Duong Vu (2009)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Thread algebra is a semantics for recent object-oriented programming languages [J.A. Bergstra and M.E. Loots, J. Logic Algebr. Program. 51 (2002) 125–156; J.A. Bergstra and C.A. Middelburg, Formal Aspects Comput. (2007)] such as C# and Java. This paper shows that thread algebra provides a process-algebraic framework for reasoning about and classifying various standard notions of noninterference, an important property in secure information flow. We will take the noninterference property given by...

Thread algebra for noninterference

Thuy Duong Vu (2008)

RAIRO - Theoretical Informatics and Applications

Thread algebra is a semantics for recent object-oriented programming languages [J.A. Bergstra and M.E. Loots, J. Logic Algebr. Program.51 (2002) 125–156; J.A. Bergstra and C.A. Middelburg, Formal Aspects Comput. (2007)] such as C# and Java. This paper shows that thread algebra provides a process-algebraic framework for reasoning about and classifying various standard notions of noninterference, an important property in secure information flow. We will take the noninterference property given...

Three notes on the complexity of model checking fixpoint logic with chop

Martin Lange (2007)

RAIRO - Theoretical Informatics and Applications

This paper analyses the complexity of model checking fixpoint logic with Chop – an extension of the modal μ-calculus with a sequential composition operator. It uses two known game-based characterisations to derive the following results: the combined model checking complexity as well as the data complexity of FLC are EXPTIME-complete. This is already the case for its alternation-free fragment. The expression complexity of FLC is trivially P-hard and limited from above by the complexity of solving...

Currently displaying 1 – 6 of 6

Page 1