CAV
2010
Springer
13 years 1 months ago
2010
Springer
CAV
2010
Springer
13 years 2 months ago
2010
Springer
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 ...
CAV
2010
Springer
13 years 2 months ago
2010
Springer
CAV
2010
Springer
13 years 2 months ago
2010
Springer
CAV
2010
Springer
13 years 2 months ago
2010
Springer
Abstract. Proofs of progress properties often require fairness assumptions. Incorporating global fairness assumptions in a compositional method is a challenge, however, given the l...
CAV
2010
Springer
13 years 4 months ago
2010
Springer
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...
CAV
2010
Springer
13 years 4 months ago
2010
Springer
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...
CAV
2010
Springer
13 years 4 months ago
2010
Springer
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...
CAV
2010
Springer
2010
Springer
Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs
13 years 6 months ago
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...
CAV
2010
Springer
13 years 6 months ago
2010
Springer
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...