Sciweavers

FUIN
2006
142views more  FUIN 2006»
13 years 3 months ago
Comparing BDD and SAT Based Techniques for Model Checking Chaum's Dining Cryptographers Protocol
Abstract. We analyse different versions of the Dining Cryptographers protocol by means of automatic verification via model checking. Specifically we model the protocol in terms of ...
Magdalena Kacprzak, Alessio Lomuscio, Artur Niewia...
IJISEC
2008
101views more  IJISEC 2008»
13 years 3 months ago
SAT-based model-checking for security protocols analysis
We present a model checking technique for security protocols based on a reduction to propositional logic. At the core of our approach is a procedure that, given a description of th...
Alessandro Armando, Luca Compagna
ENTCS
2006
112views more  ENTCS 2006»
13 years 3 months ago
Distributed Symbolic Bounded Property Checking
In this paper we describe an algorithm for distributed, BDD-based bounded property checking and its implementation in the verification tool SymC. The distributed algorithm verifie...
Pradeep Kumar Nalla, Roland J. Weiss, Prakash Moha...
ENTCS
2006
114views more  ENTCS 2006»
13 years 3 months ago
Open-Source Model Checking
We present GMC2 , a software model checker for GCC, the opensource compiler from the Free Software Foundation (FSF). GMC2 , which is part of the GMC static-analysis and model-check...
Radu Grosu, Xiaowan Huang, Sumit Jain, Scott A. Sm...
ENTCS
2008
123views more  ENTCS 2008»
13 years 3 months ago
A Multi-Core Solver for Parity Games
We describe a parallel algorithm for solving parity games, with applications in, e.g., modal
Jaco van de Pol, Michael Weber 0002
CAV
2010
Springer
185views Hardware» more  CAV 2010»
13 years 3 months ago
Achieving Distributed Control through Model Checking
Abstract. We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints on concurrent systems. We calculate when processe...
Susanne Graf, Doron Peled, Sophie Quinton
AADEBUG
1997
Springer
13 years 7 months ago
Backwards-Compatible Bounds Checking for Arrays and Pointers in C Programs
This paper presents a new approach to enforcing array bounds and pointer checking in the C language. Checking is rigorous in the sense that the result of pointer arithmetic must r...
Richard W. M. Jones, Paul H. J. Kelly
TACAS
2001
Springer
92views Algorithms» more  TACAS 2001»
13 years 8 months ago
Language Containment Checking with Nondeterministic BDDs
Abstract. Checking for language containment between nondeterministic ω-automata is a central task in automata-based hierarchical verification. We present a symbolic procedure for...
Bernd Finkbeiner
FMCAD
2004
Springer
13 years 9 months ago
Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders
This paper describes a new method that is useful in combinational equivalence checking with very challenging industrial designs. The method does not build a miter; instead it build...
In-Ho Moon, Carl Pixley
ECOOP
2004
Springer
13 years 9 months ago
Typestates for Objects
Today’s mainstream object-oriented compilers and tools do not support declaring and statically checking simple pre- and postconditions on methods and invariants on object represe...
Robert DeLine, Manuel Fähndrich