FSTTCS
2001
Springer
13 years 9 months ago
2001
Springer
Abstract. This paper addresses the state explosion problem in automata based LTL model checking. To deal with large space requirements we turn to use a distributed approach. All th...
FOSSACS
2001
Springer
13 years 9 months ago
2001
Springer
Abstract. Among the branching-time temporal logics used for the specification and verification of systems, CTL+ , FCTL and ECTL+ are the most notable logics for which the precise...
CONCUR
2001
Springer
13 years 9 months ago
2001
Springer
Bounded model checking has been recently introduced as an efficient verification method for reactive systems. In this work we apply bounded model checking to asynchronous systems....
CAV
2001
Springer
13 years 9 months ago
2001
Springer
Model Checking is an algorithmic technique to determine whether a temporal property holds of a program. For linear time properties, a model checker produces a counterexample comput...
CAV
2001
Springer
13 years 9 months ago
2001
Springer
In formal verification, we verify that a system is correct with respect to a specification. When verification succeeds and the system is proven to be correct, there is still a q...
ASP
2001
Springer
13 years 9 months ago
2001
Springer
In this paper bounded model checking of asynchronous concurrent systems is introduced as a promising application area for answer set programming. This is an extension of earlier w...
CAV
2009
Springer
13 years 9 months ago
2009
Springer
Priorities are used to control the execution of systems to meet given requirements for optimal use of resources, e.g., by using scheduling policies. For distributed systems, it is ...
ICSE
2010
IEEE-ACM
13 years 9 months ago
2010
IEEE-ACM
Though verification tools are finding industrial use, the utility of engineering optimizations that make them scalable and usable is not widely known. Despite the fact that seve...
SACMAT
2010
ACM
13 years 9 months ago
2010
ACM
The role-based access control (RBAC) has significantly simplified the management of users and permissions in computing systems. In dynamic environments, systems are usually unde...
LICS
2002
IEEE
13 years 9 months ago
2002
IEEE
istic Abstraction for Model Checking: an Approach Based on Property Testing∗ Sophie Laplante† Richard Lassaigne‡ Fr´ed´eric Magniez§ Sylvain Peyronnet† Michel de Rougemo...