| 2015 | On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control. | Chuck C. Liang, Dale Miller |
| 2015 | Proof Search in Nested Sequent Calculi. | Bjrn Lellmann, Elaine Pimentel |
| 2015 | Well-founded Functions and Extreme Predicates in Dafny: A Tutorial. | K. Rustan M. Leino |
| 2015 | Compiling Hilbert's epsilon operator. | K. Rustan M. Leino |
| 2015 | Constrained Term Rewriting tooL. | Cynthia Kop, Naoki Nishida |
| 2015 | Cobra: A Tool for Solving General Deductive Games. | Miroslav Klimos, Antonn Kucera |
| 2015 | Improving Statistical Linguistic Algorithms for Parsing Mathematics. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. | Cezary Kaliszyk, Josef Urban |
| 2015 | Finding Inconsistencies in Programs with Loops. | Temesghen Kahsai, Jorge A. Navas, Dejan Jovanovic, Martin Schf |
| 2015 | Application of Trace-Based Subjective Logic to User Preferences Modeling. | Hoang Nam Ho, Mourad Rabah, Samuel Nowakowski, Pascal Estraillier |
| 2015 | Clausal Proof Compression. | Marijn Heule, Armin Biere |
| 2015 | Compositional Propositional Proofs. | Marijn J. H. Heule, Armin Biere |
| 2015 | Reasoning About Embedded Dependencies Using Inclusion Dependencies. | Miika Hannula |
| 2015 | Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. | Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters |
| 2015 | On Anti-subsumptive Knowledge Enforcement. | ric Grgoire, Jean-Marie Lagniez |
| 2015 | Normalisation by Completeness with Heyting Algebras. | Gatan Gilbert, Olivier Hermant |
| 2015 | A Lightweight Double-negation Translation. | Frdric Gilbert |
| 2015 | Sharing HOL4 and HOL Light Proof Knowledge. | Thibault Gauthier, Cezary Kaliszyk |
| 2015 | Controller Synthesis for MDPs and Frequency LTL | Vojtech Forejt, Jan Krcl, Jan Kretnsk |
| 2015 | Automated Discovery of Simulation Between Programs. | Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina |
| 2015 | Gamifying Program Analysis. | Daniel Fava, Julien Signoles, Matthieu Lemerre, Martin Schf, Ashish Tiwari |
| 2015 | Boolean Formulas for the Static Identification of Injection Attacks in Java. | Michael D. Ernst, Alberto Lovato, Damiano Macedonio, Ciprian Spiridon, Fausto Spoto |
| 2015 | Automated Benchmarking of Incremental SAT and QBF Solvers. | Uwe Egly, Florian Lonsing, Johannes Oetsch |
| 2015 | ELPI: Fast, Embeddable, λProlog Interpreter. | Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi |
| 2015 | Decidability, Introduction Rules and Automata. | Gilles Dowek, Ying Jiang |