Abstract is missing.
- Skolemization for Substructural LogicsPetr Cintula, Denisa Diaconescu, George Metcalfe. 1-15 [doi]
- Reasoning About Embedded Dependencies Using Inclusion DependenciesMiika Hannula. 16-30 [doi]
- Cobra: A Tool for Solving General Deductive GamesMiroslav Klimos, Antonín Kucera. 31-47 [doi]
- On Anti-subsumptive Knowledge EnforcementÉric Grégoire, Jean-Marie Lagniez. 48-62 [doi]
- Value Sensitivity and Observable Abstract Values for Information Flow ControlLuciano Bello, Daniel Hedin, Andrei Sabelfeld. 63-78 [doi]
- SAT-Based Minimization of Deterministic \omega -AutomataSouheib Baarir, Alexandre Duret-Lutz. 79-87 [doi]
- FEMaLeCoP: Fairly Efficient Machine Learning Connection ProverCezary Kaliszyk, Josef Urban. 88-96 [doi]
- Decidability, Introduction Rules and AutomataGilles Dowek, Ying Jiang. 97-111 [doi]
- Analyzing Internet Routing Security Using Model CheckingAdi Sosnovich, Orna Grumberg, Gabi Nakibly. 112-129 [doi]
- Boolean Formulas for the Static Identification of Injection Attacks in JavaMichael D. Ernst, Alberto Lovato, Damiano Macedonio, Ciprian Spiridon, Fausto Spoto. 130-145 [doi]
- An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with SubexponentialsKaustuv Chaudhuri, Giselle Reis. 146-161 [doi]
- \GUVojtech Forejt, Jan Krcál, Jan Kretínský. 162-177 [doi]
- Automated Benchmarking of Incremental SAT and QBF SolversUwe Egly, Florian Lonsing, Johannes Oetsch. 178-186 [doi]
- A Labelled Sequent Calculus for Intuitionistic Public Announcement LogicShoshin Nomura, Katsuhiko Sano, Satoshi Tojo. 187-202 [doi]
- Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic ProofsPatrick Baillot, Gilles Barthe, Ugo Dal Lago. 203-218 [doi]
- TIP: Tools for Inductive ProversDan Rosén, Nicholas Smallbone. 219-232 [doi]
- Verification of Concurrent Programs Using Trace Abstraction RefinementFranck Cassez, Frowin Ziegler. 233-248 [doi]
- Synchronized Recursive Timed AutomataYuya Uezato, Yasuhiko Minamide. 249-265 [doi]
- Focused Labeled Proof Systems for Modal LogicDale Miller, Marco Volpe. 266-280 [doi]
- On CTL* with Graded Path ModalitiesBenjamin Aminof, Aniello Murano, Sasha Rubin. 281-296 [doi]
- On Subexponentials, Synthetic Connectives, and Multi-level Delimited ControlChuck Liang, Dale Miller. 297-312 [doi]
- On the Expressive Power of Communication Primitives in Parameterised SystemsBenjamin Aminof, Sasha Rubin, Florian Zuleger. 313-328 [doi]
- There Is No Best \beta -Normalization Strategy for Higher-Order ReasonersAlexander Steen, Christoph Benzmüller. 329-339 [doi]
- Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-VectorsLiana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters. 340-355 [doi]
- Abstract Domains and Solvers for Sets ReasoningArlen Cox, Bor-Yuh Evan Chang, Huisong Li, Xavier Rival. 356-371 [doi]
- Sharing HOL4 and HOL Light Proof KnowledgeThibault Gauthier, Cezary Kaliszyk. 372-386 [doi]
- Relational Reasoning via Probabilistic CouplingGilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub. 387-401 [doi]
- A Contextual Logical FrameworkPeter Brottveit Bock, Carsten Schürmann. 402-417 [doi]
- Enhancing Search-Based QBF Solving by Dynamic Blocked Clause EliminationFlorian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, Martina Seidl. 418-433 [doi]
- Reasoning About Loops Using Vampire in KeYWolfgang Ahrendt, Laura Kovács, Simon Robillard. 434-443 [doi]
- Compositional Propositional ProofsMarijn J. H. Heule, Armin Biere. 444-459 [doi]
- ELPI: Fast, Embeddable, \lambda Prolog InterpreterCvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. 460-468 [doi]
- Normalisation by Completeness with Heyting AlgebrasGaëtan Gilbert, Olivier Hermant. 469-482 [doi]
- Using Program Synthesis for Program AnalysisCristina David, Daniel Kroening, Matt Lewis. 483-498 [doi]
- Finding Inconsistencies in Programs with LoopsTemesghen Kahsai, Jorge A. Navas, Dejan Jovanovic, Martin Schäf. 499-514 [doi]
- Modular Multiset RewritingIliano Cervesato, Edmund S. L. Lam. 515-531 [doi]
- Modelling Moral Reasoning and Ethical Responsibility with Logic ProgrammingFiona Berreby, Gauvain Bourgne, Jean-Gabriel Ganascia. 532-548 [doi]
- Constrained Term Rewriting tooLCynthia Kop, Naoki Nishida 0001. 549-557 [doi]
- Proof Search in Nested Sequent CalculiBjörn Lellmann, Elaine Pimentel. 558-574 [doi]
- SHIQ TBoxesThinh Dong, Chan Le Duc, Philippe Bonnot 0002, Myriam Lamolle. 575-590 [doi]
- Gamifying Program AnalysisDaniel Fava, Julien Signoles, Matthieu Lemerre, Martin Schäf, Ashish Tiwari. 591-605 [doi]
- Automated Discovery of Simulation Between ProgramsGrigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina. 606-621 [doi]
- SAT Modulo Intuitionistic ImplicationsKoen Claessen, Dan Rosén. 622-637 [doi]