CADE 2007 - PDF Preprint Papers

CADE 2007 Automated Deduction

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CADE-2007 Paper

click to vote

CADE
2007
Springer

263views Logical Reasoning» more CADE 2007»

Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems

14 years 11 months ago

Download www.loria.fr

Manna and Pnueli have extensively shown how a mixture of first-order logic (FOL) and discrete Linear time Temporal Logic (LTL) is sufficient to precisely state verification problem...

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, D...

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	263	Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems	claim
2	219	Conservative Extensions in the Lightweight Description Logic EL	claim
3	192	T-Decision by Decomposition	claim
4	189	Logical Interpretation: Static Program Analysis Using Theorem Proving	claim
5	180	Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4	claim
6	171	Solving Quantified Verification Conditions Using Satisfiability Modulo Theories	claim
7	166	Encoding First Order Proofs in SAT	claim
8	165	Encodings of Bounded LTL Model Checking in Effectively Propositional Logic	claim
9	164	Optimized Reasoning in Description Logics Using Hypertableaux	claim
10	158	Combining Deduction and Algebraic Constraints for Hybrid System Analysis	claim
11	154	Barendregt's Variable Convention in Rule Inductions	claim
12	154	The Bedwyr System for Model Checking over Syntactic Expressions	claim
13	151	Dependency Pairs for Rewriting with Non-free Constructors	claim
14	151	The Heterogeneous Tool Set (Hets)	claim
15	149	Certified Size-Change Termination	claim
16	149	Fully Verified Java Card API Reference Implementation	claim
17	147	ALICE: An Advanced Logic for Interactive Component Engineering	claim
18	144	Inferring Invariants by Symbolic Execution	claim
19	138	First Order Reasoning on a Large Ontology	claim
20	134	Predictive Labeling with Dependency Pairs Using SAT	claim
21	133	Hyper Tableaux with Equality	claim
22	131	Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic	claim
23	129	An Incremental Technique for Automata-Based Decision Procedures	claim
24	129	Symbolic Fault Injection	claim
25	125	A Mechanization of Phylogenetic Trees	claim
26	124	The KeY system 1.0 (Deduction Component)	claim
27	122	KeY-C: A Tool for Verification of C Programs	claim
28	120	Improvements in Formula Generalization	claim
29	119	Formalization of Continuous Probability Distributions	claim
30	119	A Sequent Calculus for Integer Arithmetic with Counterexample Generation	claim
31	118	Automated Reasoning in Kleene Algebra	claim
32	117	Logical Engineering with Instance-Based Methods	claim
33	106	System Description: E-KRHyper	claim
34	106	A Termination Checker for Isabelle Hoare Logic	claim
35	102	MaLARea: a Metasystem for Automated Reasoning in Large Theories	claim
36	102	Proving Termination by Bounded Increase	claim
37	100	Efficient E-Matching for SMT Solvers	claim
38	98	Labelled Clauses	claim
39	98	System for Automated Deduction (SAD): A Tool for Proof Verification	claim
40	98	Semantic Selection of Premisses for Automated Theorem Proving	claim
41	96	Formal Device and Programming Model for a Serial Interface	claim
42	95	Handling Polymorphism in Automated Deduction	claim
43	88	A History-based Verification of Distributed Applications	claim
44	83	SRASS - A Semantic Relevance Axiom Selection System	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers