Nicola Olivetti, Ashish Tiwari 0001
Proceedings of the Eighth International Joint Conference on Automated Reasoning
IJCAR, 2016.

@proceedings{IJCAR-2016,
	doi           = "10.1007/978-3-319-40229-1",
	editor        = "Nicola Olivetti and Ashish Tiwari 0001",
	isbn          = "978-3-319-40228-4",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Eighth International Joint Conference on Automated Reasoning}",
	volume        = 9706,
	year          = 2016,
}

Contents (38 items)

IJCAR-2016-Avron #framework #logic #set

A Logical Framework for Developing and Mechanizing Set Theories (AA), pp. 3–8.

IJCAR-2016-Gulwani #algorithm #ambiguity #programming

Programming by Examples: Applications, Algorithms, and Ambiguity Resolution (SG), pp. 9–14.

IJCAR-2016-Platzer #cyber-physical #logic #proving

Logic & Proofs for Cyber-Physical Systems (AP), pp. 15–21.

IJCAR-2016-BlanchetteFW #framework #satisfiability

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (JCB, MF, CW), pp. 25–44.

IJCAR-2016-KieslSTB

Super-Blocked Clauses (BK, MS, HT, AB), pp. 45–61.

IJCAR-2016-AlbertiGP #array #constraints

Counting Constraints in Flat Array Fragments (FA, SG, EP), pp. 65–81.

IJCAR-2016-BansalRBT #constraints #finite #set #smt

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (KB, AR, CWB, CT), pp. 82–98.

IJCAR-2016-SelsamM #congruence #type system

Congruence Closure in Intensional Type Theory (DS, LdM), pp. 99–115.

IJCAR-2016-BrombergerW #constraints #performance #testing #theorem proving

Fast Cube Tests for LIA Constraint Solving (MB, CW), pp. 116–132.

IJCAR-2016-ReynoldsBCT #recursion #smt

Model Finding for Recursive Functions in SMT (AR, JCB, SC, CT), pp. 133–151.

IJCAR-2016-Sebastiani

Colors Make Theories Hard (RS), pp. 152–170.

IJCAR-2016-AotoK #confluence

Nominal Confluence Tool (TA, KK), pp. 173–182.

IJCAR-2016-DuranEEMMT #generative #maude #unification

Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 (FD, SE, SE, NMO, JM, CLT), pp. 183–192.

IJCAR-2016-GanDXZKC #polynomial #synthesis

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF (TG, LD, BX, NZ, DK, MC), pp. 195–212.

IJCAR-2016-MatsuzakiIKZFKA #benchmark #metric #problem

Race Against the Teens - Benchmarking Mechanized Math on Pre-university Problems (TM, HI, MK, YZ, RF, JK, HA, NHA), pp. 213–227.

IJCAR-2016-TungKO #constraints #named #polynomial #smt

raSAT: An SMT Solver for Polynomial Constraints (VXT, TVK, MO), pp. 228–237.

IJCAR-2016-CernaL #order #principle

Schematic Cut Elimination and the Ordered Pigeonhole Principle (DMC, AL), pp. 241–256.

IJCAR-2016-Nivelle #algorithm #geometry

Subsumption Algorithms for Three-Valued Geometric Resolution (HdN), pp. 257–272.

IJCAR-2016-Sofronie-Stokkermans #on the

On Interpolation and Symbol Elimination in Theory Extensions (VSS), pp. 273–289.

IJCAR-2016-EbnerHRRWZ

System Description: GAPT 2.0 (GE, SH, GR, MR, SW, SZ), pp. 293–301.

IJCAR-2016-Otten #named #proving

nanoCoP: A Non-clausal Connection Prover (JO), pp. 302–312.

IJCAR-2016-HoderR0V

Selecting the Selection (KH, GR, MS0, AV), pp. 313–329.

IJCAR-2016-SchulzM #heuristic #performance #proving #theorem proving

Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (SS0, MM), pp. 330–345.

IJCAR-2016-FarberB

Internal Guidance for Satallax (MF0, CEB), pp. 349–361.

IJCAR-2016-WisniewskiSKB #effectiveness #normalisation

Effective Normalization Techniques for HOL (MW, AS, KK, CB), pp. 362–370.

IJCAR-2016-Boudou #complexity #composition #logic #parallel

Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition (JB), pp. 373–388.

IJCAR-2016-BozzelliMMPS #logic #model checking

Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments (LB, AM, AM, AP, PS), pp. 389–405.

IJCAR-2016-NalonHD #multimodal #proving

: A Resolution-Based Prover for Multimodal K (CN, UH, CD), pp. 406–415.

IJCAR-2016-Ramanayake

Inducing Syntactic Cut-Elimination for Indexed Nested Sequents (RR), pp. 416–432.

IJCAR-2016-CostaM #logic

A Tableau System for Quasi-Hybrid Logic (DC, MAM), pp. 435–451.

IJCAR-2016-DawsonBG #calculus #logic #theorem #using

Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi (JED, JB, RG), pp. 452–468.

IJCAR-2016-DochertyP #graph #logic

Intuitionistic Layered Graph Logic (SD, DJP), pp. 469–486.

IJCAR-2016-ZoharZ #automation #calculus #named #satisfiability

Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi (YZ, AZ), pp. 487–495.

IJCAR-2016-AminofR #composition #model checking #multi

Model Checking Parameterised Multi-token Systems via the Composition Method (BA, SR), pp. 499–515.

IJCAR-2016-AthanasiouLW #bound #equation #thread #using #verification

Unbounded-Thread Program Verification using Thread-State Equations (KA, PL, TW), pp. 516–531.

IJCAR-2016-GuCW #composition #constraints #logic

A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints (XG, TC, ZW), pp. 532–549.

IJCAR-2016-FrohnNHBG #bound #integer #runtime #source code

Lower Runtime Bounds for Integer Programs (FF, MN, JH, MB, JG), pp. 550–567.

IJCAR-2016-HupelK #higher-order #scala #source code

Translating Scala Programs to Isabelle/HOL - System Description (LH, VK), pp. 568–577.