Maria Paola Bonacina
Proceedings of the 24th International Conference on Automated Deduction
CADE, 2013.

@proceedings{CADE-2013,
	address       = "Lake Placid, New York, USA",
	doi           = "10.1007/978-3-642-38574-2",
	editor        = "Maria Paola Bonacina",
	isbn          = "978-3-642-38573-5",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 24th International Conference on Automated Deduction}",
	volume        = 7898,
	year          = 2013,
}

Contents (33 items)

8 ×#logic
6 ×#proving
4 ×#named
3 ×#automation
3 ×#first-order
3 ×#reasoning
3 ×#verification
2 ×#composition
2 ×#constraints
2 ×#hybrid

CADE-2013-Filliatre #logic

One Logic to Use Them All (JCF), pp. 1–20.

CADE-2013-IosifRS #logic #recursion

The Tree Width of Separation Logic with Recursive Definitions (RI, AR, JS), pp. 21–38.

CADE-2013-BaumgartnerW #abstraction

Hierarchic Superposition with Weak Abstraction (PB, UW), pp. 39–57.

CADE-2013-KersaniP #decidability #first-order

Completeness and Decidability Results for First-Order Clauses with Indices (AK, NP), pp. 58–75.

CADE-2013-Mayer #hybrid #logic #proving #transitive

A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies (MCM), pp. 76–90.

CADE-2013-Comon-LundhCS #deduction

Tractable Inference Systems: An Extension with a Deducibility Predicate (HCL, VC, GS), pp. 91–108.

CADE-2013-AzmyW #normalisation

Computing Tiny Clause Normal Forms (NA, CW), pp. 109–125.

CADE-2013-BenderPS #logic

System Description: E-KRHyper 1.4 — Extensions for Unique Names and Description Logic (MB, BP, CS), pp. 126–134.

CADE-2013-BeckertGS #algorithm #logic

Analysing Vote Counting Algorithms via Logic — And Its Application to the CADE Election Scheme (BB, RG, CS), pp. 135–144.

CADE-2013-Shankar #automation #performance #reasoning

Automated Reasoning, Fast and Slow (NS), pp. 145–161.

CADE-2013-ChihaniMR #first-order #logic #proving

Foundational Proof Certificates in First-Order Logic (ZC, DM, FR), pp. 162–177.

CADE-2013-MouraP

Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals (LMdM, GOP), pp. 178–192.

CADE-2013-LoupSCAB #algebra #composition #constraints

A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition (UL, KS, FC, EÁ, BB), pp. 193–207.

CADE-2013-GaoKC #named #smt

dReal: An SMT Solver for Nonlinear Theories over the Reals (SG, SK, EMC), pp. 208–214.

CADE-2013-GangeSSS #composition #constraints #difference

Solving Difference Constraints over Modular Arithmetic (GG, HS, PJS, PS), pp. 215–230.

CADE-2013-ErbaturEKLLMMNSS #analysis #encryption #paradigm #protocol #symmetry #unification

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis (SE, SE, DK, ZL, CL, CM, JM, PN, SS, RS), pp. 231–248.

CADE-2013-ErbaturKMNR

Hierarchical Combination (SE, DK, AMM, PN, CR), pp. 249–266.

CADE-2013-KaliszykU #named #proving #re-engineering

PRocH: Proof Reconstruction for HOL Light (CK, JU), pp. 267–274.

CADE-2013-GoreT #logic

An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description (RG, JT), pp. 275–281.

CADE-2013-HawblitzelKLR #automation #proving #source code #theorem proving #towards #using

Towards Modularly Comparing Programs Using Automated Theorem Provers (CH, MK, SKL, HR), pp. 282–299.

CADE-2013-HahnleSB #reuse #verification

Reuse in Software Verification by Abstract Method Calls (RH, IS, RB), pp. 300–314.

CADE-2013-BeckertB #logic #semantics

Dynamic Logic with Trace Semantics (BB, DB), pp. 315–329.

CADE-2013-BaaderBL #data access #ontology

Temporalizing Ontology-Based Data Access (FB, SB, ML), pp. 330–344.

CADE-2013-HeuleHW #verification

Verifying Refutations with Extended Resolution (MH, WAHJ, NW), pp. 345–359.

CADE-2013-Sofronie-Stokkermans #generative #hybrid #parametricity #reasoning #verification

Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems (VSS), pp. 360–376.

CADE-2013-ReynoldsTGKDB #finite #quantifier #smt

Quantifier Instantiation Techniques for Finite Model Finding in SMT (AR, CT, AG, SK, MD, CB), pp. 377–391.

CADE-2013-ClaessenJRS #automation #induction #proving #using

Automating Inductive Proofs Using Theory Exploration (KC, MJ, DR, NS), pp. 392–406.

CADE-2013-KuhlweinSU

E-MaLeS 1.1 (DK, SS, JU), pp. 407–413.

CADE-2013-BlanchetteP #first-order #morphism #named #polymorphism

TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism (JCB, AP), pp. 414–420.

CADE-2013-WilliamsK #problem #proving #reduction #satisfiability

Propositional Temporal Proving with Reductions to a SAT Problem (RW, BK), pp. 421–435.

CADE-2013-KaminskiT #incremental #named #reasoning #reduction #satisfiability

InKreSAT: Modal Reasoning via Incremental Reduction to SAT (MK, TT), pp. 436–442.

CADE-2013-KovasznaiFB #quantifier

: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into (GK, AF, AB), pp. 443–449.

CADE-2013-HoderV

The 481 Ways to Split a Clause and Deal with Propositional Variables (KH, AV), pp. 450–464.