Sciweavers

FMCAD
2006
Springer
13 years 11 months ago
Finite Instantiations for Integer Difference Logic
The last few years have seen the advent of a new breed of decision procedures for various fragments of first-order logic based on ional abstraction. A lazy satisfiability checker ...
Hyondeuk Kim, Fabio Somenzi
FMCAD
2006
Springer
13 years 11 months ago
Post-reboot Equivalence and Compositional Verification of Hardware
We introduce a finer concept of a Hardware Machine, where the set of post-reboot operation states is explicitly a part of the FSM definition. We formalize an ad-hoc flow of combin...
Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, Z...
FMCAD
2006
Springer
13 years 11 months ago
Optimizations for LTL Synthesis
We present an approach to automatic synthesis of specifications given in Linear Time Logic. The approach is based on a translation through universal co-B
Barbara Jobstmann, Roderick Bloem
FMCAD
2006
Springer
13 years 11 months ago
Tracking MUSes and Strict Inconsistent Covers
In this paper, a new heuristic-based approach is introduced to extract minimally unsatisfiable subformulas (in short, MUSes) of SAT instances. It is shown that it often outperforms...
Éric Grégoire, Bertrand Mazure, C&ea...
FMCAD
2006
Springer
13 years 11 months ago
Assume-Guarantee Reasoning for Deadlock
Sagar Chaki, Nishant Sinha
FM
2006
Springer
124views Formal Methods» more  FM 2006»
13 years 11 months ago
Compositional Binding in Network Domains
This paper considers network services that bind identifiers in the course of delivering messages, and also persistent, point-to-point connections made in the context of such bindin...
Pamela Zave
FM
2006
Springer
97views Formal Methods» more  FM 2006»
13 years 11 months ago
Modeling and Validating Distributed Embedded Real-Time Systems with VDM++
Marcel Verhoef, Peter Gorm Larsen, Jozef Hooman
FM
2006
Springer
112views Formal Methods» more  FM 2006»
13 years 11 months ago
Interactive Verification of Medical Guidelines
Medical guidelines are useful to standardize health care. As thousands of patients are treated according to these guidelines, the quality of guidelines is an important issue. In th...
Jonathan Schmitt, Alwin Hoffmann, Michael Balser, ...
FM
2006
Springer
169views Formal Methods» more  FM 2006»
13 years 11 months ago
PSL Model Checking and Run-Time Verification Via Testers
Abstract. The paper introduces the construct of temporal testers as a compositional basis for the construction of automata corresponding to temporal formulas in the PSL logic. Temp...
Amir Pnueli, Aleksandr Zaks