Sciweavers

ATVA
2015
Springer
19views Hardware» more  ATVA 2015»
8 years 8 months ago
Severity Levels of Inconsistent Code
Inconsistent code detection is a variant of static analysis that detects statements that never occur on feasible executions. This includes code whose execution ultimately must lead...
Martin Schäf, Ashish Tiwari
ATVA
2015
Springer
25views Hardware» more  ATVA 2015»
8 years 8 months ago
Spanning the Spectrum from Safety to Liveness
Of special interest in formal verification are safety specifications, which assert that the system stays within some allowed region, in which nothing “bad” happens. Equivalen...
Rachel Faran, Orna Kupferman
ATVA
2015
Springer
37views Hardware» more  ATVA 2015»
8 years 8 months ago
Decidability of the Reachability for a Family of Linear Vector Fields
The reachability problem is one of the most important issues in the verification of hybrid systems. Computing the reachable sets of differential equations is difficult, although c...
Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, Na...
ATVA
2015
Springer
25views Hardware» more  ATVA 2015»
8 years 8 months ago
Trace Diagnostics Using Temporal Implicants
Runtime verification and model checking are two important methods for assessing correctness of systems. In both techniques, detecting an error is witnessed by an execution that vi...
Thomas Ferrère, Oded Maler, Dejan Nickovic
ATVA
2015
Springer
24views Hardware» more  ATVA 2015»
8 years 8 months ago
Lattice-Based Semantics for Combinatorial Model Evolution
Combinatorial test design (CTD) is an effective test design technique, considered to be a testing best practice. CTD provides automatic test plan generation, but it requires a man...
Rachel Tzoref-Brill, Shahar Maoz
ATVA
2015
Springer
29views Hardware» more  ATVA 2015»
8 years 8 months ago
Effective Verification of Replicated Data Types Using Later Appearance Records (LAR)
Replicated data types store copies of identical data across multiple servers in a distributed system. For the replicas to satisfy strong eventual consistency, these data types sho...
Madhavan Mukund, Gautham Shenoy R., S. P. Suresh
ATVA
2015
Springer
30views Hardware» more  ATVA 2015»
8 years 8 months ago
Game Semantic Analysis of Equivalence in IMJ
Abstract. Using game semantics, we investigate the problem of verifying contextual equivalences in Interface Middleweight Java (IMJ), an imperative object calculus in which program...
Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzeve...
ATVA
2015
Springer
20views Hardware» more  ATVA 2015»
8 years 8 months ago
Hierarchical Information Patterns and Distributed Strategy Synthesis
Abstract Infinite games with imperfect information tend to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is ...
Dietmar Berwanger, Anup Basil Mathew, Marie van de...
ASYNC
2015
IEEE
36views Hardware» more  ASYNC 2015»
8 years 8 months ago
Analyzing Isochronic Forks with Potential Causality
Abstract—Asynchrony and concurrency are fundamental notions in the fields of asynchronous circuits as well as distributed systems. This paper treats asynchronous circuits as a s...
Rajit Manohar, Yoram Moses
ASYNC
2015
IEEE
30views Hardware» more  ASYNC 2015»
8 years 8 months ago
Gate Sizing and Vth Assignment for Asynchronous Circuits Using Lagrangian Relaxation
—Gate sizing and threshold voltage selection is an important step in the VLSI physical design process to help reduce power consumption and improve circuit performance. Recent asy...
Gang Wu, Ankur Sharma, Chris C. N. Chu