Sciweavers

FSTTCS
2001
Springer
14 years 3 months ago
Distributed LTL Model Checking Based on Negative Cycle Detection
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...
Lubos Brim, Ivana Cerná, Pavel Krcál...
FOSSACS
2001
Springer
14 years 3 months ago
Model Checking CTL+ and FCTL is Hard
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...
François Laroussinie, Nicolas Markey, Ph. S...
CONCUR
2001
Springer
14 years 3 months ago
Bounded Reachability Checking with Process Semantics
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....
Keijo Heljanko
CAV
2001
Springer
119views Hardware» more  CAV 2001»
14 years 3 months ago
Certifying Model Checkers
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...
Kedar S. Namjoshi
CAV
2001
Springer
121views Hardware» more  CAV 2001»
14 years 3 months ago
A Practical Approach to Coverage in Model Checking
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...
Hana Chockler, Orna Kupferman, Robert P. Kurshan, ...
ASP
2001
Springer
14 years 3 months ago
Answer Set Programming and Bounded Model Checking
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...
Keijo Heljanko, Ilkka Niemelä
CAV
2009
Springer
116views Hardware» more  CAV 2009»
14 years 3 months ago
Priority Scheduling of Distributed Systems Based on Model Checking
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 ...
Ananda Basu, Saddek Bensalem, Doron Peled, Joseph ...
ICSE
2010
IEEE-ACM
14 years 3 months ago
An empirical study of optimizations in YOGI
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...
Aditya V. Nori, Sriram K. Rajamani
SACMAT
2010
ACM
14 years 3 months ago
Role updating for assignments
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...
Jinwei Hu, Yan Zhang, Ruixuan Li, Zhengding Lu
LICS
2002
IEEE
14 years 3 months ago
Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing
istic Abstraction for Model Checking: an Approach Based on Property Testing∗ Sophie Laplante† Richard Lassaigne‡ Fr´ed´eric Magniez§ Sylvain Peyronnet† Michel de Rougemo...
Sophie Laplante, Richard Lassaigne, Fréd&ea...