Nikolaj Bjørner, Viorica Sofronie-Stokkermans
Proceedings of the 23rd International Conference on Automated Deduction
CADE, 2011.
@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.
7 ×#logic
7 ×#proving
6 ×#automation
4 ×#reasoning
4 ×#smt
3 ×#analysis
3 ×#first-order
3 ×#theorem proving
2 ×#complexity
2 ×#data type
7 ×#proving
6 ×#automation
4 ×#reasoning
4 ×#smt
3 ×#analysis
3 ×#first-order
3 ×#theorem proving
2 ×#complexity
2 ×#data type