|
CAV
|
ICLP
|
IJCAR
|
| |
| |
|
08:45‑09:30 (Grand Ballroom B)
Herbrand Award: Wolfgang Bibel |
09:00‑09:30 (Grand Ballroom C)
Vineet Kahlon, Aarti Gupta and Nishant Sinha
Symbolic Model Checking of Concurrent Programs using Partial Orders and
On-the-fly Transactions
|
09:00‑09:30 (Grand Ballroom A)
Péter Szabó
and Péter Szeredi
Improving the ISO Prolog standard by analysing compliance test results
|
09:30‑10:00 (Grand Ballroom C)
Koushik Sen
and Mahesh Viswanathan
Model Checking Multithreaded Programs with Asynchronous Atomic Methods
|
09:30‑10:30 (Grand Ballroom A)
Christopher A. Welty
Semantic Web: The story of the RIFt so far
|
09:30‑09:45 (Grand Ballroom B)
Juergen Giesl
, Peter Schneider-Kamp
and Rene Thiemann
AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework
|
09:45‑10:00 (Grand Ballroom B)
Boontawee Suntisrivaraporn
, Franz Baader
and Carsten Lutz
CEL---A Practical Reasoner for Life Science Ontologies
|
10:00‑10:30 (Grand Ballroom C)
Azadeh Farzan
and P. Madhusudan
Causal Atomicity
|
10:00‑10:15 (Grand Ballroom B)
Dmitry Tsarkov and Ian Horrocks
FaCT++ Description Logic Reasoner: System Description
|
10:15‑10:30 (Grand Ballroom B)
Steven Obua
and Sebastian Skalberg
Importing HOL into Isabelle/HOL
|
10:30‑11:00
Break |
11:00‑11:30 (Grand Ballroom C)
Rajeev Alur
, Swarat Chaudhuri
and P. Madhusudan
Languages of Nested Trees
|
11:00‑11:30 (Grand Ballroom A)
Martin Brain
, Tom Crick
, Marina De Vos
and John Fitch
TOAST: Applying Answer Set Programming to Superoptimisation
|
11:00‑11:30 (Willow A)
Hans de Nivelle
and Jia Meng
Geometric Resolution: A Proof Procedure Based on Finite Model Search
|
11:00‑11:30 (Grand Ballroom B)
Roy Dyckhoff
, Delia Kesner
and Stephane Lengrand
Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic
|
11:30‑12:00 (Grand Ballroom C)
Akash Lal
and Thomas Reps
Improving Pushdown System Model Checking
|
11:30‑12:00 (Grand Ballroom A)
Susanne Grell, Torsten Schaub
and Joachim Selbig
Modelling biological networks by action languages via answer set programming
|
11:30‑12:00 (Willow A)
Xiang Xue Jia and Jian Zhang
A Powerful Technique to Eliminate Isomorphism in Finite Model Search
|
11:30‑12:00 (Grand Ballroom B)
Brigitte Pientka
Eliminating redundancy in higher-order unification:a lightweight approach
|
12:00‑12:30 (Grand Ballroom C)
Andreas Griesmayer
, Roderick Bloem
and Byron Cook
Repair of Boolean Programs with an Application to C
|
12:00‑12:30 (Grand Ballroom A)
Petra Schwaiger
and Burkhard Freitag
Using Answer Set Programming for the Automatic Compilation of Assessment Tests
|
12:00‑12:30 (Willow A)
Adam Koprowski
and Hans Zantema
Recursive Path Ordering for Infinite Labelled Rewrite Systems
|
12:00‑12:30 (Grand Ballroom B)
Florian Rabe
First-Order Logic with Dependent Types
|
12:30‑14:00 (Grand Ballroom D)
Lunch (in hotel) |
12:30‑14:00
Lunch break |
12:30‑14:00 (Grand Ballroom D)
Lunch (in hotel) |
14:00‑14:30 (Grand Ballroom C)
Mark Braverman
Termination of Integer Linear Programs
|
14:00‑14:30 (Grand Ballroom A)
Maarten van Emden
Compositional Semantics for the Procedural Interpretation of Logic
|
14:00‑14:30 (Grand Ballroom B)
Erik Reeber
and Warren A. Hunt, Jr.
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
|
14:00‑14:30 (Willow A)
Dexter Kozen
, Christoph Kreitz and Eva Richter
Automating Proofs in Category Theory
|
14:30‑15:00 (Grand Ballroom C)
Josh Berdine
, Byron Cook
, Dino Distefano
and Peter O'Hearn
Automatic termination proofs for programs with shape-shifting heaps
|
14:30‑15:00 (Grand Ballroom A)
Luke Simon, Ajay Mallya, Ajay Bansal and Gopal Gupta
Coinductive Logic Programming
|
14:30‑15:00 (Grand Ballroom B)
Shuvendu Lahiri
and Madanlal Musuvathi
Solving Sparse Linear Constraints
|
14:30‑15:00 (Willow A)
Roland Zumkeller
Formal Global Optimisation with Taylor Models
|
15:00‑15:30 (Grand Ballroom C)
Panagiotis Manolios
and Daron Vroon
Termination Analysis with Calling Context Graphs
|
15:00‑15:30 (Grand Ballroom A)
Pedro Cabalar
, Sergei Odintsov, David Pearce and Agustin Valverde
Analysing and Extending Well-Founded and Partial Stable Semantics using Partial Equilibrium Logic
|
15:00‑15:30 (Grand Ballroom B)
Olga Grinchtein, Martin Leucker
and Nir Piterman
Inferring Network Invariants Automatically
|
15:00‑15:30 (Willow A)
Benjamin Grégoire
and Laurent Théry
A purely functional library for modular arithmetic and its application to certifying large prime numbers
|
15:30‑15:45 (Grand Ballroom C)
Byron Cook
, Andreas Podelski and Andrey Rybalchenko
Terminator: Beyond Safety
|
15:30‑16:00 (Grand Ballroom A)
James Cheney
The Semantics of Nominal Logic Programs
|
15:30‑16:00 (Grand Ballroom B)
Christian Urban
and Stefan Berghofer
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
|
15:30‑16:00 (Willow A)
Assia Mahboubi
Proving formally the implementation of an efficient gcd algorithm for polynomials
|
15:45‑16:00 (Grand Ballroom C)
Koushik Sen
and Gul Agha
CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools
|
16:00‑16:30
Break |
16:30‑17:30 (Grand Ballroom B/C)
David Harel
Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs [ppt]
|
| |
|
|
17:45‑19:00 (Grand Ballroom A)
ALP Business Meeting |
18:00‑19:00 (Grand Ballroom C)
CAV Business Meeting |
18:00‑20:00 (Grand Ballroom B)
IJCAR Business Meeting |
| |
|
