Leonardo de Moura
Proceedings of the 26th International Conference on Automated Deduction
CADE, 2017.

@proceedings{CADE-2017,
	doi           = "10.1007/978-3-319-63046-5",
	editor        = "Leonardo de Moura",
	isbn          = "['978-3-319-63045-8', '978-3-319-63046-5']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 26th International Conference on Automated Deduction}",
	volume        = 10395,
	year          = 2017,
}

Contents (34 items)

CADE-2017-Andronick #concurrent #reasoning

Reasoning About Concurrency in High-Assurance, High-Performance Software Systems (JA), pp. 1–7.

CADE-2017-SantosGMN #javascript #source code #towards #verification

Towards Logic-Based Verification of JavaScript Programs (JFS, PG, PM, DN), pp. 8–25.

CADE-2017-PassmoreI #algorithm #verification

Formal Verification of Financial Algorithms (GOP, DI), pp. 26–41.

CADE-2017-BonacinaGS #modulo theories #satisfiability

Satisfiability Modulo Theories and Assignments (MPB, SGL, NS), pp. 42–59.

CADE-2017-ErbaturMR

Notions of Knowledge in Combinations of Theories Sharing Constructors (SE, AMM, CR), pp. 60–76.

CADE-2017-HorbachVW #integer #linear #on the

On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic (MH, MV, CW), pp. 77–94.

CADE-2017-CimattiGIRS #incremental #satisfiability

Satisfiability Modulo Transcendental Functions via Incremental Linearization (AC, AG, AI, MR, RS), pp. 95–113.

CADE-2017-Cruanes #bound #satisfiability

Satisfiability Modulo Bounded Checking (SC), pp. 114–129.

CADE-2017-HeuleKB #proving

Short Proofs Without New Variables (MJHH, BK, AB), pp. 130–147.

CADE-2017-MengRTB #constraints #relational #smt #theorem proving

Relational Constraint Solving in SMT (BM, AR, CT, CWB), pp. 148–165.

CADE-2017-BenderS #metric #set

Decision Procedures for Theories of Sets with Measures (MB, VSS), pp. 166–184.

CADE-2017-CristiaR #set #strict

A Decision Procedure for Restricted Intensional Sets (MC, GR), pp. 185–201.

CADE-2017-TeuckeW #constraints #decidability #first-order #linear #monad

Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints (AT, CW), pp. 202–219.

CADE-2017-Cruz-FilipeHHKS #performance #verification

Efficient Certified RAT Verification (LCF, MJHH, WAHJ, MK, PSK), pp. 220–236.

CADE-2017-Lammich #performance #satisfiability

Efficient Verified (UN)SAT Certificate Checking (PL), pp. 237–254.

CADE-2017-BlancoCM #proving

Translating Between Implicit and Explicit Versions of Proof (RB, ZC, DM0), pp. 255–273.

CADE-2017-Kiesl0 #first-order #logic

A Unifying Principle for Clause Elimination in First-Order Logic (BK, MS0), pp. 274–290.

CADE-2017-GleissK0 #proving

Splitting Proofs for Interpolation (BG, LK, MS0), pp. 291–309.

CADE-2017-0001SUP #consistency #detection #first-order #knowledge base #nondeterminism #scalability

Detecting Inconsistencies in Large First-Order Knowledge Bases (SS0, GS, JU, AP), pp. 310–325.

CADE-2017-HustadtOD #logic #metric #proving #theorem proving

Theorem Proving for Metric Temporal Logic over the Naturals (UH, AO, CD), pp. 326–343.

CADE-2017-ItegulovSP #proving #theorem proving

Scavenger 0.1: A Theorem Prover Based on Conflict Resolution (DI, JS, BWP), pp. 344–356.

CADE-2017-PapapanagiotouF #composition #framework #named #process #specification #workflow

WorkflowFM: A Logic-Based Framework for Formal Process Specification and Composition (PP, JDF), pp. 357–370.

CADE-2017-LonsingE #search-based

DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL (FL, UE), pp. 371–384.

CADE-2017-NageleFM #named

CSI: New Evidence - A Progress Report (JN, BF, AM), pp. 385–397.

CADE-2017-BarbosaBF #fine-grained #proving #scalability

Scalable Fine-Grained Proofs for Formula Processing (HB, JCB, PF), pp. 398–412.

CADE-2017-SternagelS #confluence #term rewriting

Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems (CS, TS), pp. 413–431.

CADE-2017-BeckerBWW #higher-order

A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms (HB, JCB, UW, DW), pp. 432–453.

CADE-2017-BrockschmidtJT0 #integer #proving #safety #termination

Certifying Safety and Termination Proofs for Integer Transition Systems (MB, SJCJ, RT, AY0), pp. 454–471.

CADE-2017-BrotherstonGK #array #logic #problem

Biabduction (and Related Problems) in Array Separation Logic (JB, NG, MIK), pp. 472–490.

CADE-2017-TellezB #automation #pointer #proving #source code #verification

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof (GT, JB), pp. 491–508.

CADE-2017-XuCW #composition #constraints #logic #satisfiability

Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints (ZX, TC, ZW), pp. 509–527.

CADE-2017-NagashimaK #generative #higher-order #proving

A Proof Strategy Language and Proof Script Generation for Isabelle/HOL (YN, RK), pp. 528–545.

CADE-2017-EchenimP #formal method

The Binomial Pricing Model in Finance: A Formalization in Isabelle (ME, NP), pp. 546–562.

CADE-2017-FarberKU #monte carlo #proving

Monte Carlo Tableau Proof Search (MF0, CK, JU), pp. 563–579.