Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
ENTCS
2006
131views more  ENTCS 2006»
10 years 11 months ago
Development Separation in Lambda-Calculus
We present a proof technique in -calculus that can facilitate inductive reasoning on -terms by separating certain -developments from other -reductions. We give proofs based on thi...
Hongwei Xi
ENTCS
2006
125views more  ENTCS 2006»
10 years 11 months ago
Liveness Checking as Safety Checking for Infinite State Spaces
In previous work we have developed a syntactic reduction of repeated reachability to reachability for finite state systems. This may lead to simpler and more uniform proofs for mo...
Viktor Schuppan, Armin Biere
ENTCS
2006
106views more  ENTCS 2006»
10 years 11 months ago
Probabilistic Observations and Valuations: (Extended Abstract)
d Abstract) 1 Matthias Schr
Matthias Schröder, Alex Simpson
ENTCS
2006
133views more  ENTCS 2006»
10 years 11 months ago
A Compositional Natural Semantics and Hoare Logic for Low-Level Languages
The advent of proof-carrying code has generated significant interest in reasoning about low-level languages. It is widely believed that low-level languages with jumps must be diff...
Ando Saabas, Tarmo Uustalu
ENTCS
2006
111views more  ENTCS 2006»
10 years 11 months ago
A Verified Compiler for Synchronous Programs with Local Declarations
In addition to efficient code generation, causality cycles and schizophrenic statements are major problems for the compilation of synchronous programs. Although these problems are ...
Klaus Schneider, Jens Brandt, Tobias Schüle
ENTCS
2006
124views more  ENTCS 2006»
10 years 11 months ago
A New Rabin-type Trapdoor Permutation Equivalent to Factoring
Public key cryptography has been invented to overcome some key management problems in open networks. Although nearly all aspects of public key cryptography rely on the existence of...
Katja Schmidt-Samoa
ENTCS
2006
125views more  ENTCS 2006»
10 years 11 months ago
An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving
To broaden the scope of decision procedures for linear arithmetic, they have to be integrated into theorem provers. Successful approaches e.g. in NQTHM or ACL2 suggest a close int...
Tobias Schmidt-Samoa
ENTCS
2006
92views more  ENTCS 2006»
10 years 11 months ago
Nonstandard Meromorphic Groups
Extending the work of [7] on groups definable in compact complex manifolds and of [1] on strongly minimal groups definable in nonstandard compact complex manifolds, we classify al...
Thomas Scanlon
ENTCS
2006
104views more  ENTCS 2006»
10 years 11 months ago
Abstract Graph Transformation
Arend Rensink, Dino Distefano
ENTCS
2006
180views more  ENTCS 2006»
10 years 11 months ago
Mobile Synchronizing Petri Nets: A Choreographic Approach for Coordination in Ubiquitous Systems
The term Ubiquitous Computing was coined by Mark Weiser almost two decades ago. Despite all the time that has passed since Weiser's vision, ubiquitous computing still has a l...
Fernando Rosa Velardo, Olga Marroquín Alons...
books