|
CASC
|
CAV
|
ICLP
|
IJCAR
|
| |
| |
09:00‑10:00 (Metropolitan A)
Tony Hoare
The Ideal of Verified Software [ppt]
|
09:00‑10:00 (Cirrus)
Brigitte Pientka
Overcoming performance barriers: efficient verification techniques for logical frameworks [pdf]
|
09:00‑09:15 (Metropolitan B)
Jürgen Zimmer
and Serge Autexier
The MathServe Framework for Semantic Web Reasoning Services
|
09:15‑09:30 (Metropolitan B)
Predrag Janicic
and Pedro Quaresma
System Description: GCLCprover + GeoThms
|
09:30‑09:45 (Metropolitan B)
Joe Hendrix
, Jose Meseguer and Hitoshi Ohsaki
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms
|
09:45‑10:00 (Metropolitan B)
Allen Van Gelder
and Geoff Sutcliffe
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
|
09:50‑10:00 (Willow A)
The CASC panel, Entrants, Everyone who's interested
Start of competition (at 10:00, continues through the break)
|
10:00‑10:30
Break |
10:30‑12:30 (Willow A)
The ATP systems
Competition running live, results on the big screen (continues through lunch)
|
10:30‑11:00 (Metropolitan A)
Kenneth McMillan
Lazy Abstraction with Interpolants
|
10:30‑11:00 (Cirrus)
Andy King
, Lunjin Lu and Samir Genaim
Detecting Determinacy in Prolog Programs
|
10:30‑11:00 (Metropolitan B)
Robert Constable
and Wojciech Moczydlowski
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
|
11:00‑11:30 (Metropolitan A)
Himanshu Jain
, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter
and Chao Wang
Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop
|
11:00‑11:30 (Cirrus)
Xuan Li, Andy King
and Lunjin Lu
Collapsing Closures
|
11:00‑11:30 (Metropolitan B)
John Harrison
Towards self-verification of HOL Light
|
11:30‑12:00 (Metropolitan A)
Daniel Kroening
and Georg Weissenbacher
Counterexamples with Loops for Predicate Abstraction
|
11:30‑12:00 (Cirrus)
Elvira Albert
, Puri Arenas
, German Puebla
and Manuel Hermenegildo
Reduced Certificates for Abstraction-Carrying Code
|
11:30‑12:00 (Metropolitan B)
Sean McLaughlin
An Interpretation of Isabelle/HOL in HOL Light
|
12:00‑12:15 (Metropolitan A)
Nikhil Sethi
and Clark Barrett
Cascade: C Assertion Checker and Deductive Engine
|
12:00‑12:30 (Cirrus)
Alberto Pettorossi
, Maurizio Proietti
and Valerio Senni
Proving Properties of Constraint Logic Programs by Eliminating Existential Variables
|
12:00‑12:30 (Metropolitan B)
Chad E. Brown
Combining Type Theory and Untyped Set Theory
|
12:15‑12:30 (Metropolitan A)
Arie Gurfinkel
, Ou Wei and marsha chechik
Yasm: A Software Model-Checker for Verification and Refutation
|
12:30‑14:00
Lunch break |
14:00‑16:30 (Willow A)
The ATP systems
Competition running live, results on the big screen (continues through the break)
|
14:00‑14:30 (Metropolitan A)
Jan-Willem Roorda
and Koen Claessen
SAT-based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation
|
14:00‑14:30 (Cirrus)
Enrico Pontelli and Tran Son
Justifications for Logic Programs under Answer Set Semantics
|
14:00‑14:30 (Metropolitan B)
Christoph Benzmüller
, Chad E. Brown
and Michael Kohlhase
Cut-Simulation in Impredicative Logics
|
14:30‑15:00 (Metropolitan A)
Rachel Tzoref and Orna Grumberg
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
|
14:30‑15:00 (Cirrus)
Katsumi Inoue
and Chiaki Sakama
Generality Relations in Answer Set Programming
|
14:30‑15:00 (Metropolitan B)
Viorica Sofronie-Stokkermans
Interpolation in local theory extensions
|
15:00‑15:30 (Metropolitan A)
Doron Bustan
and John Havlicek
Some complexity results for SystemVerilog Assertions
|
15:00‑15:30 (Cirrus)
Davy Van Nieuwenborgh
, Stijn Heymans and Dirk Vermeir
Cooperating Answer Set Programming
|
15:00‑15:30 (Metropolitan B)
Anna Zamansky
and Arnon Avron
Canonical Gentzen-type calculi with (n,k)-ary quantifiers
|
15:30‑16:00 (Metropolitan A)
Jochen Klose, Tobe Toben, Bernd Westphal and Hartmut Wittke
Check It Out: On the Efficient Formal Verification of Live Sequence Charts
|
15:30‑16:00 (Cirrus)
Johan Wittocx, Joost Vennekens
, Maarten Mariën
, Marc Denecker
and Maurice Bruynooghe
Predicate Introduction under Stable and Well-founded Semantics
|
15:30‑16:00 (Metropolitan B)
Bernhard Beckert
and Andre Platzer
Dynamic Logic with Non-rigid Functions
|
16:00‑16:30
Break |
16:30‑17:00 (Willow A)
The ATP systems
Competition should end in this session, final results on the big screen
|
16:30‑17:00 (Metropolitan A)
Marta Kwiatkowska
, Gethin Norman
and David Parker
Symmetry Reduction for Probabilistic Model Checking
|
16:30‑17:30 (Cirrus)
Monica Lam
Why Use Datalog to Analyze Programs? [ppt]
|
16:30‑17:30 (Metropolitan B)
Adnan Darwiche
Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation [ppt]
|
| |
17:00‑17:30 (Metropolitan A)
Pavel Krcal
and Wang Yi
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
|
17:30‑18:00 (Metropolitan A)
Grigore Rosu
and Saddek Bensalem
Allen Linear (Interval) Temporal Logic -- Translation to LTL and Monitor Synthesis
|
|
|
18:00‑18:15 (Metropolitan A)
Jiri Barnat, Lubos Brim, Ivana Cerna, Pavel Moravec, Petr Rockai and Pavel Simecek
DiVinE - A Tool for Distributed Verification
|
18:15‑18:30 (Metropolitan A)
Flavio M. de Paula
and Alan Hu
EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation
|
| |
19:00‑19:30 (depart Spirit of Seattle from Pier 55)
CAV-IJCAR Joint Cruise/Banquet
Boarding from Pier 55 (walking distance from hotel)
|
19:00‑22:00 (Cirrus)
ICLP Banquet |
19:00‑19:30 (depart Spirit of Seattle from Pier 55)
CAV-IJCAR Joint Cruise/Banquet
Boarding from Pier 55 (walking distance from hotel)
|
19:30‑22:30 (depart Spirit of Seattle from Pier 55)
CAV-IJCAR Joint Cruise/Banquet
|
19:30‑22:30 (depart Spirit of Seattle from Pier 55)
CAV-IJCAR Joint Cruise/Banquet
|
| |
