Proceedings of the 23rd International Conference on Automated Deduction
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

Nikolaj Bjørner, Viorica Sofronie-Stokkermans
Proceedings of the 23rd International Conference on Automated Deduction
CADE, 2011.

TEST
DBLP
Scholar
DOI
Full names Links ISxN
@proceedings{CADE-2011,
	address       = "Wroclaw, Poland",
	doi           = "10.1007/978-3-642-22438-6",
	editor        = "Nikolaj Bjørner and Viorica Sofronie-Stokkermans",
	isbn          = "978-3-642-22437-9",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 23rd International Conference on Automated Deduction}",
	volume        = 6803,
	year          = 2011,
}

Contents (38 items)

CADE-2011-Claessen #automation #first-order #logic #reasoning
The Anatomy of Equinox — An Extensible Automated Reasoning Tool for First-Order Logic and Beyond — (KC), pp. 1–3.
CADE-2011-Cook #liveness #proving #roadmap #termination
Advances in Proving Program Termination and Liveness (BC), p. 4.
CADE-2011-Ranta #logic #what
Translating between Language and Logic: What Is Easy and What Is Difficult (AR), pp. 5–25.
CADE-2011-AlbertiAR #analysis #automation #named #policy #security
ASASP: Automated Symbolic Analysis of Security Policies (FA, AA, SR), pp. 26–33.
CADE-2011-AlpuenteBER #logic #slicing
Backward Trace Slicing for Rewriting Logic Theories (MA, DB, JE, DR), pp. 34–48.
CADE-2011-ArnaudCD #protocol #recursion #security #testing
Deciding Security for Protocols with Recursive Tests (MA, VC, SD), pp. 49–63.
CADE-2011-AspertiRCT #interactive #proving #theorem proving
The Matita Interactive Theorem Prover (AA, WR, CSC, ET), pp. 64–69.
CADE-2011-BaaderBBM #concept #logic #unification
Unification in the Description Logic EL without the Top Concept (FB, TBN, SB, BM), pp. 70–84.
CADE-2011-BaumgartnerT #evolution #similarity
Model Evolution with Equality Modulo Built-in Theories (PB, CT), pp. 85–100.
CADE-2011-BiereLS
Blocked Clause Elimination for QBF (AB, FL, MS), pp. 101–115.
CADE-2011-BlanchetteBP #smt
Extending Sledgehammer with SMT Solvers (JCB, SB, LCP), pp. 116–130.
CADE-2011-BrotherstonDP #automation #logic #proving
Automated Cyclic Entailment Proofs in Separation Logic (JB, DD, RLP), pp. 131–146.
CADE-2011-Brown #higher-order #problem #proving #satisfiability #sequence #theorem proving
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (CEB), pp. 147–161.
CADE-2011-Burel #deduction
Experimenting with Deduction Modulo (GB), pp. 162–176.
CADE-2011-BohmeM #automation #challenge #data type #proving
Heaps and Data Structures: A Challenge for Automated Provers (SB, MM), pp. 177–191.
CADE-2011-ChortarasTS #owl #query
Optimized Query Rewriting for OWL 2 QL (AC, DT, GBS), pp. 192–206.
CADE-2011-ClaessenLS #first-order #logic
Sort It Out with Monotonicity — Translating between Many-Sorted and Unsorted First-Order Logic (KC, AL, NS), pp. 207–221.
CADE-2011-DeharbeFMP #problem #smt #symmetry
Exploiting Symmetry in SMT Problems (DD, PF, SM, BWP), pp. 222–236.
CADE-2011-FontaineMP #proving
Compression of Propositional Resolution Proofs via Partial Regularization (PF, SM, BWP), pp. 237–251.
CADE-2011-FredriksonCJ #algorithm #analysis #approximate #behaviour #complexity
Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms (MF, MC, SJ), pp. 252–267.
CADE-2011-GalmicheM
A Connection-Based Characterization of Bi-intuitionistic Validity (DG, DM), pp. 268–282.
CADE-2011-HaarslevSV #automation #reasoning #smt
Automated Reasoning in 𝒜ℒ𝒞𝒬 via SMT (VH, RS, MV), pp. 283–298.
CADE-2011-HoderV #reasoning #scalability
Sine Qua Non for Large Theory Reasoning (KH, AV), pp. 299–314.
CADE-2011-Horbach #horn clause #set
Predicate Completion for non-Horn Clause Sets (MH), pp. 315–330.
CADE-2011-Horbach11a
System Description: SPASS-FD (MH), pp. 331–337.
CADE-2011-JovanovicM #integer #linear
Cutting to the Chase Solving Linear Integer Arithmetic (DJ, LMdM), pp. 338–353.
CADE-2011-KlinovP #hybrid #probability #satisfiability
A Hybrid Method for Probabilistic Satisfiability (PK, BP), pp. 354–368.
CADE-2011-KorovinV #bound #linear
Solving Systems of Linear Inequalities by Bound Propagation (KK, AV), pp. 369–383.
CADE-2011-KovacsMV #on the #order
On Transfinite Knuth-Bendix Orders (LK, GM, AV), pp. 384–399.
CADE-2011-KoksalKS #power of #programming #scala #smt
Scala to the Power of Z3: Integrating SMT and Programming (ASK, VK, PS), pp. 400–406.
CADE-2011-LiuL #morphism #performance #unification
Efficient General Unification for XOR with Homomorphism (ZL, CL), pp. 407–421.
CADE-2011-NoschinskiEG #analysis #complexity #dependence #framework #term rewriting
A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems (LN, FE, JG), pp. 422–438.
CADE-2011-PayetS #android #source code #static analysis
Static Analysis of Android Programs (ÉP, FS), pp. 439–445.
CADE-2011-Platzer #difference #hybrid #logic #probability #source code
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs (AP), pp. 446–460.
CADE-2011-SchneiderS #automation #first-order #ontology #owl #proving #reasoning #theorem proving #using
Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving (MS, GS), pp. 461–475.
CADE-2011-WiesMK #data type #imperative #performance
An Efficient Decision Procedure for Imperative Tree Data Structures (TW, MM, VK), pp. 476–491.
CADE-2011-WinklerM #termination #tool support
AC Completion with Termination Tools (SW, AM), pp. 492–498.
CADE-2011-ZanklFM #confluence #named
CSI — A Confluence Tool (HZ, BF, AM), pp. 499–505.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.