Sciweavers

Share
CAV
2010
Springer
140views Hardware» more  CAV 2010»
8 years 11 months ago
PARAM: A Model Checker for Parametric Markov Models
Ernst Moritz Hahn, Holger Hermanns, Björn Wac...
CAV
2010
Springer
227views Hardware» more  CAV 2010»
9 years 20 days ago
Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems
We describe Breach, a Matlab toolbox providing a coherent set of simulation-based techniques aimed at the analysis of deterministic models of hybrid dynamical systems. The primary ...
Alexandre Donzé
CAV
2010
Springer
159views Hardware» more  CAV 2010»
9 years 20 days ago
On Array Theory of Bounded Elements
Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu
CAV
2010
Springer
143views Hardware» more  CAV 2010»
9 years 20 days ago
Jtlv: A Framework for Developing Verification Algorithms
Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck
CAV
2010
Springer
168views Hardware» more  CAV 2010»
9 years 20 days ago
A Dash of Fairness for Compositional Reasoning
Abstract. Proofs of progress properties often require fairness assumptions. Incorporating global fairness assumptions in a compositional method is a challenge, however, given the l...
Ariel Cohen 0002, Kedar S. Namjoshi, Yaniv Sa'ar
CAV
2010
Springer
156views Hardware» more  CAV 2010»
9 years 2 months ago
A Logical Product Approach to Zonotope Intersection
We define and study a new abstract domain which is a fine-grained combination of zonotopes with (sub-)polyhedric domains such as the interval, ocinear template or polyhedron domain...
Khalil Ghorbal, Eric Goubault, Sylvie Putot
CAV
2010
Springer
286views Hardware» more  CAV 2010»
9 years 2 months ago
ABC: An Academic Industrial-Strength Verification Tool
ABC is a public-domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous hardware designs. ABC combines scalable logic transforma...
Robert K. Brayton, Alan Mishchenko
CAV
2010
Springer
185views Hardware» more  CAV 2010»
9 years 2 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
CAV
2010
Springer
239views Hardware» more  CAV 2010»
9 years 4 months ago
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs
Triggering errors in concurrent programs is a notoriously difficult task. A key reason for this is the behavioral complexity resulting from the large number of interleavings of op...
Vineet Kahlon, Chao Wang
CAV
2010
Springer
176views Hardware» more  CAV 2010»
9 years 5 months ago
Lazy Annotation for Program Testing and Verification
Abstract. We describe an interpolant-based approach to test generation and model checking for sequential programs. The method generates Floyd/Hoare style annotations of the program...
Kenneth L. McMillan
books