CAV
2008
Springer
13 years 6 months ago
2008
Springer
This is the first system description of the Barcelogic SMT solver, which implements all techniques that our group has been developing over the last four years as well as state-of-t...
CAV
2008
Springer
13 years 6 months ago
2008
Springer
Power gating is a technique for low power design in which whole sections of the chip are powered off when they are not needed, and powered back on when they are. Functional correct...
CAV
2008
Springer
13 years 6 months ago
2008
Springer
CAV
2008
Springer
13 years 6 months ago
2008
Springer
We consider an extension of integer linear arithmetic with a "star" operator takes closure under vector addition of the solution set of a linear arithmetic subformula. We...
CAV
2008
Springer
13 years 6 months ago
2008
Springer
Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and shar...
CAV
2008
Springer
13 years 6 months ago
2008
Springer
The growing design-productivity gap has made designers shift toward using high-level languages like C, C++ and Java to do system-level design. High-Level Synthesis (HLS) is the pro...
CAV
2008
Springer
13 years 6 months ago
2008
Springer
We describe Thor (Tool for Heap-Oriented Reasoning), a tool based on separation logic that is capable of reasoning automatically about heap-manipulating programs. There are several...
CAV
2008
Springer
13 years 6 months ago
2008
Springer
We propose a type system for lock-freedom in the -calculus, which guarantees that certain communications will eventually succeed. Distinguishing features of our type system are: it...
CAV
2008
Springer
13 years 6 months ago
2008
Springer
Hangal et. al. [3] have developed a procedure to check if an instance of the execution of a shared memory multiprocessor program, is consistent with the Total Store Order (TSO) mem...
CAV
2008
Springer
13 years 6 months ago
2008
Springer
Counterexample-guided abstraction refinement (CEGAR) has been en vogue for the automatic verification of very large systems in the past years. When trying to apply CEGAR to the ver...