Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CAV
2004
Springer
93views Hardware» more  CAV 2004»
11 years 5 months ago
Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures
—We introduce a new BDD-like data structure called Hybrid-Restriction Diagrams (HRDs) for the representation and manipulation of linear hybrid automata (LHA) state-spaces and pre...
Farn Wang
CAV
2004
Springer
120views Hardware» more  CAV 2004»
11 years 5 months ago
Termination of Linear Programs
We show that termination of a class of linear loop programs is decidable. Linear loop programs are discrete-time linear systems with a loop condition governing termination, that is...
Ashish Tiwari
CAV
2004
Springer
99views Hardware» more  CAV 2004»
11 years 5 months ago
Range Allocation for Separation Logic
Abstract. Separation Logic consists of a Boolean combination of predicates of the form vi ≥ vj +c where c is a constant and vi, vj are variables of some ordered infinite type li...
Muralidhar Talupur, Nishant Sinha, Ofer Strichman,...
CAV
2004
Springer
202views Hardware» more  CAV 2004»
11 years 5 months ago
Statistical Model Checking of Black-Box Probabilistic Systems
Abstract. We propose a new statistical approach to analyzing stochastic systems against specifications given in a sublogic of continuous stochastic logic (CSL). Unlike past numeri...
Koushik Sen, Mahesh Viswanathan, Gul Agha
CAV
2004
Springer
87views Hardware» more  CAV 2004»
11 years 5 months ago
GSTE Is Partitioned Model Checking
Verifying whether an ω-regular property is satisfied by a finite-state system is a core problem in model checking. Standard techniques build an automaton with the complementary ...
Roberto Sebastiani, Eli Singerman, Stefano Tonetta...
CAV
2004
Springer
104views Hardware» more  CAV 2004»
11 years 5 months ago
Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings
Abstract. We present an unfolding-based approach to LTL-X modelchecking of high-level Petri nets. It is based on the method proposed by Esparza and Heljanko for low-level nets [4, ...
Claus Schröter, Victor Khomenko
CAV
2004
Springer
159views Hardware» more  CAV 2004»
11 years 5 months ago
Static Program Analysis via 3-Valued Logic
This paper reviews the principles behind the paradigm of “abstract interpretation via § -valued logic,” discusses recent work to extend the approach, and summarizes ongoing re...
Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm
CAV
2004
Springer
100views Hardware» more  CAV 2004»
11 years 5 months ago
An Experimental Evaluation of Ground Decision Procedures
Leonardo Mendonça de Moura, Harald Rue&szli...
CAV
2004
Springer
123views Hardware» more  CAV 2004»
11 years 5 months ago
SAL 2
SAL 2 augments the specification language and explicit-state model checker of SAL 1 with high-performance symbolic and bounded model checkers, and with novel infinite bounded and...
Leonardo Mendonça de Moura, Sam Owre, Haral...
CAV
2004
Springer
101views Hardware» more  CAV 2004»
11 years 5 months ago
Symbolic Model Checking of Non-regular Properties
This paper presents a symbolic model checking algorithm for Fixpoint Logic with Chop, an extension of the modal µ-calculus capable of defining non-regular properties. Some empiri...
Martin Lange
books