This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
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...
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 ...
Marcello M. Bonsangue, Georgiana Caltais, Eugen-Io...
Designers of concurrent and distributed algorithms usually express them using pseudo-code. In contrast, most verification techniques are based on more mathematically-oriented forma...
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...
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....