Sciweavers

ENTCS
2006
104views more  ENTCS 2006»
13 years 11 months ago
Synthesising Features by Games
Dimitar P. Guelev, Mark Dermot Ryan, Pierre-Yves S...
ENTCS
2006
161views more  ENTCS 2006»
13 years 11 months ago
Tool Building Requirements for an API to First-Order Solvers
Effective formal verification tools require that robust implementations of automatic procedures for first-order logic and satisfiability modulo theories be integrated into express...
Jim Grundy, Thomas F. Melham, Sava Krstic, Sean Mc...
ENTCS
2006
112views more  ENTCS 2006»
13 years 11 months ago
Patterns for Timed Property Specifications
Patterns for property specification enable non-experts to write formal specifications that can be used for automatic model checking. The existing patterns identified in [6] allow ...
Volker Gruhn, Ralf Laue
ENTCS
2006
114views more  ENTCS 2006»
13 years 11 months ago
Open-Source Model Checking
We present GMC2 , a software model checker for GCC, the opensource compiler from the Free Software Foundation (FSF). GMC2 , which is part of the GMC static-analysis and model-check...
Radu Grosu, Xiaowan Huang, Sumit Jain, Scott A. Sm...
ENTCS
2006
121views more  ENTCS 2006»
13 years 11 months ago
A Hierarchy of SOS Rule Formats
nary abstract) Jan Friso Groote 1 MohammadReza Mousavi 2 Michel A. Reniers 3 Department of Computer Science, Eindhoven University of Technology (TU/e), P.O. Box 513, NL-5600 MB Ein...
Jan Friso Groote, Mohammad Reza Mousavi, Michel A....
ENTCS
2006
104views more  ENTCS 2006»
13 years 11 months ago
Paradigm as Organization-Oriented Coordination Language
Global component behaviours as distinguished in Paradigm, offer the ingredients for specifying inter-component coordination in separation from and consistent with detailed compone...
Luuk Groenewegen, A. W. Stam, Pieter J. Toussaint,...
ENTCS
2006
117views more  ENTCS 2006»
13 years 11 months ago
A Formalization of Credit and Responsibility Within the GNDC Schema
We formally define a notion of credit and responsibility within the Generalized Non Deducibility on Compositions framework. We investigate the validity of our definitions through ...
Roberto Gorrieri, Fabio Martinelli, Marinella Petr...
ENTCS
2006
176views more  ENTCS 2006»
13 years 11 months ago
Automatic Formal Synthesis of Hardware from Higher Order Logic
A compiler that automatically translates recursive function definitions in higher order logic to clocked synchronous hardware is described. Compilation is by mechanised proof in t...
Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Sl...
ENTCS
2006
123views more  ENTCS 2006»
13 years 11 months ago
From Discrete Duration Calculus to Symbolic Automata
The goal of this paper is to translate (fragments of) the quantified discrete duration calculus QDDC, proposed by P. Pandya, into symbolic acceptors with counters. Acceptors are w...
Laure Gonnord, Nicolas Halbwachs, Pascal Raymond
ENTCS
2006
142views more  ENTCS 2006»
13 years 11 months ago
Specialization of Interaction Protocols in a Temporal Action Logic
Temporal logics are well suited for the specification and verification of systems of communicating agents. In this paper we adopt a social approach to agent communication, where c...
Laura Giordano, Alberto Martelli, Camilla Schwind