AMAST
2006
Springer
13 years 6 months ago
2006
Springer
We present DO-Casl, a new member of the CASL family of specification languages. It is an extension of Casl-Ltl and it supports a methodology for conveniently writing loose specific...
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
Abstract. When designing an open system, there might be no implementation available for certain components at verification time. For such systems, verification has to be based on a...
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
Abstract. In this paper we present the ITP/OCL tool, a rewritingbased tool that supports automatic validation of UML class diagrams with respect to OCL constraints. Its implementat...
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
This article demonstrates how a powerful and expressive ion from concurrency theory--monads of resumptions--plays a dual r^ole as a programming tool for concurrent applications. Th...
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
Interpretation of FIFO Queues Tristan Le Gall, Bertrand Jeannet, and Thierry J
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
Abstract. Symmetry reduced model checking is hindered by two problems: how to identify state space symmetry when systems are not fully symmetric, and how to determine equivalence o...
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
Abstract. State space explosion is the hardest challenge to the effective application of model checking methods. We present a new technique for achieving drastic state space reduct...
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
Synthesizing a proper implementation for a scenario-based specification is often impossible, due to the distributed nature of implementations. To be able to detect problematic spec...
AMAST
2006
Springer
13 years 8 months ago
2006
Springer
We propose two characterizations of complexity classes by means of programming languages. The first concerns Logspace while the second leads to Ptime. This latter characterization ...