Sciweavers

CAV
2003
Springer
107views Hardware» more  CAV 2003»
14 years 4 months ago
Theorem Proving Using Lazy Proof Explication
Many verification problems reduce to proving the validity of formulas involving both propositional connectives and domain-specific functions and predicates. This paper presents ...
Cormac Flanagan, Rajeev Joshi, Xinming Ou, James B...
CAV
2003
Springer
116views Hardware» more  CAV 2003»
14 years 4 months ago
Reasoning with Temporal Logic on Truncated Paths
We consider the problem of reasoning with linear temporal logic on truncated paths. A truncated path is a path that is finite, but not necessarily maximal. Truncated paths arise n...
Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lus...
CAV
2003
Springer
145views Hardware» more  CAV 2003»
14 years 4 months ago
Monitoring Temporal Rules Combined with Time Series
Run-time monitoring of temporal properties and assertions is used for testing and as a component of execution-based model checking techniques. Traditional run-time monitoring howev...
Doron Drusinsky
CAV
2003
Springer
124views Hardware» more  CAV 2003»
14 years 4 months ago
Evidence Explorer: A Tool for Exploring Model-Checking Proofs
Yifei Dong, C. R. Ramakrishnan, Scott A. Smolka
CAV
2003
Springer
108views Hardware» more  CAV 2003»
14 years 4 months ago
Linear Invariant Generation Using Non-linear Constraint Solving
Abstract. We present a new method for the generation of linear invariants which reduces the problem to a non-linear constraint solving problem. Our method, based on Farkas’ Lemma...
Michael Colón, Sriram Sankaranarayanan, Hen...
CAV
2003
Springer
154views Hardware» more  CAV 2003»
14 years 4 months ago
Structural Symbolic CTL Model Checking of Asynchronous Systems
In previous work, we showed how structural information can be used to efficiently generate the state-space of asynchronous systems. Here, we apply these ideas to symbolic CTL model...
Gianfranco Ciardo, Radu Siminiceanu
CAV
2003
Springer
140views Hardware» more  CAV 2003»
14 years 4 months ago
TLQSolver: A Temporal Logic Query Checker
Marsha Chechik, Arie Gurfinkel
CAV
2003
Springer
122views Hardware» more  CAV 2003»
14 years 4 months ago
Timed Control with Partial Observability
We consider the problem of synthesizing controllers for timed systems modeled using timed automata. The point of departure from earlier work is that we consider controllers that ha...
Patricia Bouyer, Deepak D'Souza, P. Madhusudan, An...
CAV
2003
Springer
97views Hardware» more  CAV 2003»
14 years 4 months ago
Iterating Transducers in the Large (Extended Abstract)
Bernard Boigelot, Axel Legay, Pierre Wolper
CAV
2003
Springer
120views Hardware» more  CAV 2003»
14 years 4 months ago
Hybrid Acceleration Using Real Vector Automata (Extended Abstract)
Bernard Boigelot, Frédéric Herbretea...