Tomasz Truderung.
Regular Protocols and Attacks with Regular Knowledge
Greta Yorsh and Madan Musuvathi.
A Combination Method for Generating Interpolants
Ullrich Hustadt, Boris Konev and Renate A. Schmidt.
Deciding monodic fragments by temporal resolution
Guillaume Dufay, Amy Felty and Stan Matwin.
Privacy-Sensitive Information Flow with JML
Viktor Kuncak, Hai, Huu Nguyen and Martin Rinard.
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
Franz Baader and Silvio Ghilardi.
Connecting many-sorted theories
Claudio Castellini and Alan Smaill.
Proof Planning for First-Order Temporal Logic
Graham Steel.
Deduction with XOR Constraints in Security API Modelling
Tal Lev-Ami, Neil Immerman, Siddharth Srivastava, Greta Yorsh, Mooly Sagiv and Thomas W. Reps.
Simulating Reachability using First-Order Logic with Applications to
Verification of Linked Data Structures
Viorica Sofronie-Stokkermans.
Hierarchic reasoning in local theory extensions
Kaustuv Chaudhuri and Frank Pfenning.
A Focusing Inverse Method Prover for First-Order Linear Logic
Mizuhito Ogawa, Eiichi Horita and Satoshi Ono.
Proving Properties of Incremental Merkel Trees
Evelyne Contejean and Pierre Corbineau.
Reflecting Proofs in First-Order Logic with Equality
Chad Brown.
Reasoning in Extensional Type Theory with Equality
Christian Fermüller and Reinhard Pichler.
Model Representation via Contexts and Implicit Generalizations
Peter Baumgartner and Cesare Tinelli.
ME-E -- The Model Evolution Calculus with Equality
Brigitte Pientka.
Tabling for higher-order logic programming
Christian Urban and Christine Tasson.
Nominal Techniques in Isabelle/HOL
Kumar Neeraj Verma, Helmut Seidl and Thomas Schwentick.
On the Complexity of Equational Horn Clauses
Jordi Levy, Mateu Villaret and Joachim Niehren.
Well-Nested Context Unification
Serge R. Autexier.
The CORE Calculus
Guillem Godoy and Ashish Tiwari.
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing,
and Right-Ground Rules
Jian Zhang.
Computer Search for Counterexamples to Wilkie's Identity
John Harrison and Sean McLaughlin.
A Proof Producing Decision Procedure for Real Arithmetic
Ting Zhang, Henny Sipma and Zohar Manna.
The Decidability of the First-order theory of Knuth-Bendix Order
accepted system descriptions
Sean Bechhofer, Ian Horrocks and Daniele Turi.
The OWL Instance Store (System Description)
Andreas Meier and Erica Melis.
MULTI: A Multi-Strategy Proof Planner (System Description)
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz and Roberto Sebastiani.
MathSAT 3 (System Description)
Marco Benedetti.
sKizzo: A Suite to Evaluate and Certify QBFs (System Description)
Alex Sinner and Thomas Kleemann.
KRHyper - In Your Pocket (System Description)
