We present a trace-driven SMT-based symbolic debugging tool for MCAPI (Multicore Association Communication API) applications. MCAPI is a newly proposed standard that provides an AP...
We study recursive timed automata that extend timed automata with recursion. Timed automata, as introduced by Alur and Dill, are finite automata accompanied by a finite set of real...
Probabilistic B (pB) [2, 8] extends classical B [7] to incorporate probabilistic updates together with the specification of quantitative safety properties. As for classical B, prob...
Abstract. It is well known that modelchecking and satisfiability of Linear Temporal Logic (LTL) are Pspace-complete. Wolper showed that with grammar operators, this result can be e...
Abstract. This paper is concerned with a method for computing reachable sets of linear continuous systems with uncertain input. Such a method is required for verification of hybrid...
Abstract. We present a first-order theory of (finite) sequences with integer elements, Presburger arithmetic, and regularity constraints, which can model significant properties of ...