CAV 2010 - PDF Preprint Papers

CAV 2010 International Workshop on Computer Aided Verification

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CAV-2010 Paper

click to vote

CAV
2010
Springer

286views Hardware» more CAV 2010»

ABC: An Academic Industrial-Strength Verification Tool

13 years 11 months ago

Download www.eecs.berkeley.edu

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

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	286	ABC: An Academic Industrial-Strength Verification Tool	claim
2	282	A NuSMV Extension for Graded-CTL Model Checking	claim
3	251	Automated Assume-Guarantee Reasoning through Implicit Learning	claim
4	243	libalf: The Automata Learning Framework	claim
5	239	Model Checking of Linearizability of Concurrent List Implementations	claim
6	239	Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs	claim
7	227	Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems	claim
8	225	Merit: An Interpolating Model-Checker	claim
9	223	RATSY - A New Requirements Analysis Tool with Synthesis	claim
10	214	Learning Component Interfaces with May and Must Abstractions	claim
11	214	Comfusy: A Tool for Complete Functional Synthesis	claim
12	207	Petruchio: From Dynamic Networks to Nets	claim
13	206	Dynamic Cutoff Detection in Parameterized Concurrent Programs	claim
14	201	Contessa: Concurrency Testing Augmented with Symbolic Analysis	claim
15	198	Termination Analysis with Compositional Transition Invariants	claim
16	198	Automatically Proving Linearizability	claim
17	197	Abstract Analysis of Symbolic Executions	claim
18	194	LTSmin: Distributed and Symbolic Reachability	claim
19	192	Invariant Synthesis for Programs Manipulating Lists with Unbounded Data	claim
20	190	Measuring and Synthesizing Systems in Probabilistic Environments	claim
21	187	Fences in Weak Memory Models	claim
22	185	Achieving Distributed Control through Model Checking	claim
23	181	Policy Monitoring in First-Order Temporal Logic	claim
24	181	Bounded Underapproximations	claim
25	179	Generating Litmus Tests for Contrasting Memory Consistency Models	claim
26	176	Robustness in the Presence of Liveness	claim
27	176	Lazy Annotation for Program Testing and Verification	claim
28	173	A Model Checker for AADL	claim
29	172	Symbolic Bounded Synthesis	claim
30	172	Quantifier Elimination by Lazy Model Enumeration	claim
31	168	A Dash of Fairness for Compositional Reasoning	claim
32	161	Directed Proof Generation for Machine Code	claim
33	159	Gist: A Solver for Probabilistic Games	claim
34	159	On Array Theory of Bounded Elements	claim
35	158	Model-Checking Parameterized Concurrent Programs Using Linear Interfaces	claim
36	158	Dsolve: Safety Verification via Liquid Types	claim
37	157	The Static Driver Verifier Research Platform	claim
38	157	Local Verification of Global Invariants in Concurrent Programs	claim
39	156	A Logical Product Approach to Zonotope Intersection	claim
40	154	Verifying Low-Level Implementations of High-Level Datatypes	claim
41	153	There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code	claim
42	146	Fast Acceleration of Ultimately Periodic Relations	claim
43	143	Jtlv: A Framework for Developing Verification Algorithms	claim
44	141	Retrofitting Legacy Code for Security	claim
45	140	PARAM: A Model Checker for Parametric Markov Models	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers