|
LICS
|
RTA
|
SAT
|
| |
08:45‑09:00 (Grand Ballroom C)
Introduction and Welcome
|
09:00‑10:00 (Grand Ballroom C)
Randal E. Bryant
Formal Verification of Infinite State Systems using Boolean Methods [ppt]
|
10:00‑10:30
Break |
10:30‑11:00 (Grand Ballroom C)
Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin
and Claire David
Two-Variable Logic on Words with Data
|
10:30‑11:00 (Willow A/B)
Michael Codish
, Vitaly Lagoon and Peter Stuckey
Solving Partial Order Constraints for LPO Termination
|
10:30‑11:00 (Grand Ballroom D)
Arist Kojevnikov
and Alexander S. Kulikov
Complexity of Semialgebraic Proofs with Restricted Degree of Falsity
|
11:00‑11:30 (Grand Ballroom C)
Stephane Demri
and Ranko Lazic
LTL with the Freeze Quantifier and Register Automata
|
11:00‑11:30 (Willow A/B)
Traian Serbanuta
and Grigore Rosu
Computationally Equivalent Elimination of Conditions
|
11:00‑11:30 (Grand Ballroom D)
Oliver Kullmann
, Ines Lynce
and Joao Marques-Silva
Categorisation of clauses in conjunctive normal forms:
Minimally unsatisfiable sub-clause-sets and the lean kernel
|
11:30‑12:00 (Grand Ballroom C)
Guoqiang Pan and Moshe Y. Vardi
Fixed-Parameter Hierarchies inside PSPACE
|
11:30‑12:00 (Willow A/B)
Sergio Antoy
, Daniel Brown and Su-Hui Chiang
On the Correctness of Bubbling
|
11:30‑11:45 (Grand Ballroom D)
Alexander Nadel
, Nachum Dershowitz
and Ziyad Hanna
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
|
11:45‑12:00 (Grand Ballroom D)
Joshua Buresh-Oppenheim
and David Mitchell
Minimum Witnesses for Unsatisfiable 2CNFs
|
12:00‑12:30 (Grand Ballroom C)
Martin Otto
The boundedness problem for monadic universal first-order logic
|
12:00‑12:30 (Willow A/B)
Joe Hendrix
, Hitoshi Ohsaki
and Mahesh Viswanathan
Propositional Tree Automata
|
12:00‑12:15 (Grand Ballroom D)
Allen Van Gelder
Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs
|
12:15‑12:30 (Grand Ballroom D)
Toni Jussila, Carsten Sinz
and Armin Biere
Extended Resolution Proofs for Symbolic SAT Solving with Quantification
|
12:30‑14:00
Lunch break |
14:00‑14:30 (Grand Ballroom C)
Marcelo Fiore
and Sam Staton
A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics
|
14:00‑14:30 (Willow A/B)
Bernhard Gramlich
and Salvador Lucas
Generalizing Newman's Lemma for Left-Linear Rewrite Systems
|
14:00‑14:30 (Grand Ballroom D)
Mark Chavira and Adnan Darwiche
Pre-Processing CNFs to Enhance Component Analysis
|
14:30‑15:00 (Grand Ballroom C)
Catuscia Palamidessi
, Vijay Saraswat
, Frank D. Valencia
and Björn Victor
On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi-Calculus
|
14:30‑15:00 (Willow A/B)
Piotr Hoffman
Unions of Equational Monadic Theories
|
14:30‑15:00 (Grand Ballroom D)
Himanshu Jain
, Constantinos Bartzis and Edmund Clarke
Satisfiability Checking of Non-clausal Formulas using General Matings
|
15:00‑15:30 (Grand Ballroom C)
Filippo Bonchi
, Ugo Montanari
and Barbara König
Saturated Semantics for Reactive Systems
|
15:00‑15:30 (Willow A/B)
Jean-Pierre Jouannaud
Modular Church-Rosser Modulo
|
15:00‑15:15 (Grand Ballroom D)
Eugene Goldberg
Determinization of resolution by an algorithm operating on complete assignments
|
15:15‑15:30 (Grand Ballroom D)
Hantao Zhang
A Complete Random Jump Strategy with Guiding Paths
|
15:30‑16:00
Break |
16:00‑16:30 (Grand Ballroom C)
Luke Ong
On model-checking trees generated by higher-order recursion schemes
|
16:00‑16:30 (Willow A/B)
Yannick Chevalier and Michael Rusinowitch
Hierarchical Combination of Intruder Theories
|
16:00‑16:30 (Grand Ballroom D)
Ilya Mironov and Lintao Zhang
Applications of SAT-Solvers to Cryptanalysis
|
16:30‑17:00 (Grand Ballroom C)
Dietrich Kuske
and Markus Lohrey
Monadic chain logic over iterations and applications
to pushdown systems
|
16:30‑17:00 (Willow A/B)
Yohan Boichut
and Thomas Genet
Feasible Trace Reconstruction for Rewriting Approximations
|
16:30‑17:00 (Grand Ballroom D)
Yuliya Zabiyaka and Adnan Darwiche
Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies
|
17:00‑17:30 (Grand Ballroom C)
Vineet Kahlon and Aarti Gupta
An Automata-theoretic Appraoch for Model Checking Threads for LTL Properties
|
17:00‑18:00 (Willow A/B)
RTA Business Meeting |
17:00‑17:15 (Grand Ballroom D)
Roberto Sebastiani
and Michele Vescovi
Encoding the satisfiability of modal and description logics into SAT:
the case study of K(m)/ALC
|
17:15‑17:30 (Grand Ballroom D)
Ines Lynce
and Joao Marques-Silva
SAT in Bioinformatics: Making the Case with Haplotype Inference
|
17:30‑18:00 (Grand Ballroom C)
Tachio Terauchi and Alex Aiken
On Typability for Rank-2 Intersection Types with Polymorphic Recursion
|
|
18:00‑19:00 (Grand Ballroom C)
LICS Business Meeting |
|
18:00‑20:00 (Richmond (4th floor))
SAT Business Meeting |
| |
