CAV 2008 - PDF Preprint Papers

CAV 2008 International Workshop on Computer Aided Verification

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CAV-2008 Paper

click to vote

CAV
2008
Springer

170views Hardware» more CAV 2008»

Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations

13 years 6 months ago

Download www.cs.cmu.edu

Abstract. The use of Craig interpolants has enabled the development of powerful hardware and software model checking techniques. Efficient algorithms are known for computing interp...

Himanshu Jain, Edmund M. Clarke, Orna Grumberg

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	170	Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations	claim
2	170	Local Proofs for Linear-Time Properties of Concurrent Programs	claim
3	161	Constraint-Based Approach for Analysis of Hybrid Systems	claim
4	160	Scalable Shape Analysis for Systems Code	claim
5	158	Linear Arithmetic with Stars	claim
6	157	Effective Program Verification for Relaxed Memory Models	claim
7	152	Heap Assumptions on Demand	claim
8	144	The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis	claim
9	143	Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems	claim
10	139	CSIsat: Interpolation for LA+EUF	claim
11	131	Validating High-Level Synthesis	claim
12	130	A Hybrid Type System for Lock-Freedom of Mobile Processes	claim
13	125	A Practical Approach to Word Level Model Checking of Industrial Netlists	claim
14	125	Application of Formal Word-Level Analysis to Constrained Random Simulation	claim
15	122	Thread Quantification for Concurrent Shape Analysis	claim
16	121	The Barcelogic SMT Solver	claim
17	115	An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths	claim
18	113	Producing Short Counterexamples Using "Crucial Events"	claim
19	112	Automated Assume-Guarantee Reasoning by Abstraction Refinement	claim
20	110	Abstract Interpretation with Applications to Timing Validation	claim
21	110	Monotonic Abstraction for Programs with Dynamic Memory Heaps	claim
22	110	Probabilistic CEGAR	claim
23	108	Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis	claim
24	106	Computing Differential Invariants of Hybrid Systems as Fixedpoints	claim
25	105	THOR: A Tool for Reasoning about Shape and Arithmetic	claim
26	104	Semi-external LTL Model Checking	claim
27	104	Proving Conditional Termination	claim
28	99	Functional Verification of Power Gated Designs by Compositional Reasoning	claim
29	99	Correcting a Space-Efficient Simulation Algorithm	claim
30	96	Implied Set Closure and Its Application to Memory Consistency Verification	claim
31	96	Conflict-Tolerant Features	claim
32	96	Monitoring Atomicity in Concurrent Programs	claim
33	89	Faster Than Uppaal?	claim
34	89	Inferring Congruence Equations Using SAT	claim
35	80	Ranking Automata and Games for Prioritized Requirements	claim
36	78	QMC: A Model Checker for Quantum Systems	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers