SBMF
2010
Springer
13 years 1 months ago
2010
Springer
This paper presents a framework to reason about the eects of assignments in recursive data structures. We dene an operational semantics for a core language based on Meyer's id...
SBMF
2010
Springer
13 years 1 months ago
2010
Springer
A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analogue of Kleene's theorem and Kleene algebra, were recently proposed ...
SBMF
2010
Springer
13 years 1 months ago
2010
Springer
Designers of concurrent and distributed algorithms usually express them using pseudo-code. In contrast, most verification techniques are based on more mathematically-oriented forma...
SBMF
2010
Springer
13 years 1 months ago
2010
Springer
ProB is a model checker for high-level formalisms such as B, Event-B, CSP and Z. ProB uses a mixed depth-first/breadth-first search strategy, and in previous work we have argued th...
SBMF
2010
Springer
13 years 1 months ago
2010
Springer
Abstract. In the context of the EU project Mobius on Proof Carrying Code for Java programs (midlets) on mobile devices, we present a way to express midlet navigation graphs in JML....
SBMF
2010
Springer
13 years 1 months ago
2010
Springer
