Abstract. The Implicit Path Enumeration Technique (IPET) has become widely accepted as a powerful technique to compute upper bounds on the Worst-Case Execution Time (WCET) of time-...
Abstract. The Operational Transformation (OT) approach, used in many collaborative editors, allows a group of users to concurrently update replicas of a shared object and exchange ...
Though program verification is known and has been used for decades, the verification of a complete computer system still remains a grand challenge. Part of this challenge is the in...
Abstract. Event-B provides us with a powerful framework for correctby-construction system development. However, while developing dependable systems we should not only guarantee the...
In this paper we describe techniques for the specification and verification of model transformations using a combination of UML and formal methods. The use of UML 2 notations to s...
Handling changes to programs and specifications efficiently is a particular challenge in formal software verification. Change impact analysis is an approach to this challenge where...
Safe is a first-order eager functional language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts...
Javier de Dios, Manuel Montenegro, Ricardo Pe&ntil...
This paper considers the model of Time Petri Nets (TPNs) extended with time parameters and its use to perform on-line diagnosis of distributed systems. We propose to base the metho...
Bartosz Grabiec, Louis-Marie Traonouez, Claude Jar...
SMT solvers have traditionally been based on the DPLL(T) algorithm, where the driving force behind the procedure is a DPLL search over truth valuations. This traditional framework ...
This paper presents extensions of Safraless algorithms proposed in the literature for automata on infinite untimed words to the case of automata on infinite timed words.
Barbara Di Giampaolo, Gilles Geeraerts, Jean-Fran&...