86
Voted
TSE
2002
14 years 10 months ago
2002
The Inequality Necessary Condition Analyzer (INCA) is a finite-state verification tool that has been able to check properties of some very large concurrent systems. INCA checks a p...
92
Voted
DEDS
2007
14 years 10 months ago
2007
The unfolding of a concurrent system represents in a compact manner all possible runs of this system. Unfoldings are used in many applications, ranging from model-checking (offlin...
74
Voted
IANDC
2008
14 years 11 months ago
2008
The main goal of this paper is to apply rewriting termination technology --enjoying a quite mature set of termination results and tools-- to the problem of proving automatically t...
121
Voted
FORTE
1994
15 years 5 days ago
1994
Critical safety and liveness properties of a concurrent system can often be proven with the help of a reachability analysis of a finite state model. This type of analysis is usual...
102
Voted
FORTE
2007
15 years 9 days ago
2007
This paper proposes an algorithm which, given a set of observations of an existing concurrent system that has repetitive subfunctions, constructs a Message Sequence Charts (MSC) gr...
88
Voted
ACSD
2008
IEEE
15 years 26 days ago
2008
IEEE
The design of complex concurrent systems often involves intricate performance and dependability considerations. Continuous-time Markov chains (CTMCs) are widely used models for co...
92
Voted
ISCIS
2005
Springer
15 years 4 months ago
2005
Springer
Abstract. Given a set of observations of an existing concurrent system with repetitive sub-functions, we consider the construction of an MSC graph representing the functionality of...
106
Voted
TABLEAUX
2007
Springer
15 years 5 months ago
2007
Springer
Abstract. Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the sys...