On this page:
Invited Speakers
- Andreas R. Blass
Adapting Logics - Randal E. Bryant
Formal Verification of Infinite State Systems using Boolean Methods - John W. Dawson
Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science - Andrew D. Gordon
Provable Implementations of Security Protocols - Orna Kupferman
Avoiding Determinization - Dana S. Scott
The Future of Proof
Invited Papers
- Andreas Blass
Adapting LogicsMore Information... - Randal E. Bryant
Formal Verification of Infinite State Systems Using Boolean MethodsMore Information... - John W. Dawson
Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer ScienceMore Information... - Andrew D. Gordon
Provable Implementations of Security ProtocolsMore Information... - Orna Kupferman
Avoiding DeterminizationMore Information...
Presented Papers
Entries are ordered by surname of first author
- Thomas Ball Orna Kupferman
An Abstraction-Refinement Framework for Multi-Agent SystemsMore Information... - Adam Barth John C. Mitchell
Managing Digital Rights using Linear LogicMore Information... - Mikołaj Bojańczyk Thomas Colcombet
Omega-Regular Expressions with BoundsMore Information... - Mikołaj Bojańczyk Anca Muscholl Thomas Schwentick Luc Segoufin Claire David
Two-Variable Logic on Words with DataMore Information... - Filippo Bonchi Ugo Montanari Barbara König
Saturated Semantics for Reactive SystemsMore Information... - Patricia Bouyer Thomas Brihaye Fabrice Chevalier
Control in o-minimal hybrid systemsMore Information... - Tomáš Brázdil Václav Brozek Vojtech Forejt Antonín Kučera
Stochastic Games with Branching-Time Winning ObjectivesMore Information... - Laura Chaubard Jean-Eric Pin Howard Straubing
First order formulas with modular predicatesMore Information... - Thierry Coquand Arnaud Spiwack
Proof of strong normalisation using domain theoryMore Information... - Ugo Dal Lago
Context Semantics, Linear Logic and Computational ComplexityMore Information... - Anuj Dawar Martin Grohe Stephan Kreutzer Nicole Schweikardt
Approximation Schemes for First-Order Definable Optimization ProblemsMore Information... - Stéphane Demri Ranko Lazic
LTL with the Freeze Quantifier and Register AutomataMore Information... - Mariangiola Dezani-Ciancaglini Makoto Tatsuta
Normalisation is insensible to lambda-term identity or differenceMore Information... - Marcelo P. Fiore Sam Staton
A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational SemanticsMore Information... - Eldar Fischer Frédéric Magniez Michel de Rougemont
Approximate Satisfiability and EquivalenceMore Information... - Jonathan Hayman Glynn Winskel
Independence and Concurrent Separation LogicMore Information... - Marcin Jurdzinski Ashutosh Trivedi
Average Time GamesMore Information... - Vineet Kahlon Aarti Gupta
An Automata-theoretic Appraoch for Model Checking Threads for LTL PropertiesMore Information... - Emil Kiss Matthew Valeriote
On tractability and congruence distributivityMore Information... - Dexter C. Kozen
Coinductive Proof Principles for Stochastic ProcessesMore Information... - Orna Kupferman Moshe Y. Vardi
Memoryful Branching-Time LogicMore Information... - Dietrich Kuske Markus Lohrey
Monadic chain logic over iterations and applications to pushdown systemsMore Information... - Benoit Larose Cynthia Loten Claude Tardif
A Characterisation of First-Order Constraint Satisfaction ProblemsMore Information... - Soren B. Lassen
Head normal form bisimulation for pairs and the lambda-mu calculusMore Information... - Olivier Laurent Lorenzo Tortora de Falco
Obsessional cliques: a semantic characterization of bounded time complexityMore Information... - Daniel Leivant
Matching explicit and modal reasoning about programs: a proof theoretic delineation of dynamic logicMore Information... - Alexis Maciel Toniann Pitassi
A Conditional Lower Bound for a System of Constant-Depth Proofs with Modular ConnectivesMore Information... - Giulio Manzonetto Antonino Salibra
Boolean algebras for lambda calculusMore Information... - C.-H. Luke Ong
On model-checking trees generated by higher-order recursion schemesMore Information... - Martin Otto
The boundedness problem for monadic universal first-order logicMore Information... - Catuscia Palamidessi Vijay A. Saraswat Frank D. Valencia Björn Victor
On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi-CalculusMore Information... - Guoqiang Pan Moshe Y. Vardi
Fixed-Parameter Hierarchies inside PSPACEMore Information... - Matthew Parkinson Richard Bornat Cristiano Calcagno
Variables as Resource in Hoare LogicsMore Information... - Nir Piterman
From Nondeterministic Büchi and Streett Automata to Deterministic Parity AutomataMore Information... - Nir Piterman Amir Pnueli
Faster Solutions of Street and Rabin GamesMore Information... - Lutz Schröder Dirk Pattinson
PSPACE reasoning for coalgebraic modal logicMore Information... - Sharon Shoham Orna Grumberg
3-Valued Abstraction: More Precision at Less CostMore Information... - Tachio Terauchi Alexander Aiken
On Typability for Rank-2 Intersection Types with Polymorphic RecursionMore Information... - Daniele Varacca Hagen Völzer
Temporal logics and model checking for fairly correct systemsMore Information...
Short Presentations
Entries are ordered by surname of first author
- Guillaume Burel Claude Kirchner
An Abstract Completion Procedure for Cut Elimination in Deduction ModuloMore Information... - Leona F. Fass
A Logical Look at Agents' Problem-Solving on the Semantic WebMore Information... - Aaron Hunter
Non-Closure Results for First-Order SpectraMore Information... - Detlef Kähler Ralf Küsters Thomas Wilke
A Dolev-Yao-based Definition of Abuse-free ProtocolsMore Information... - Roberto Maieli Paul Ruet
Interactive correctness criterion for multiplicative-additive proof-netsMore Information... - Murray Patterson Yongmei Liu Eugenia Ternovska Arvind Gupta
Grounding for Model Expansion in k-Guarded FormulasMore Information... - Jørgen Villadsen
Nominalization in Intensional Type TheoryMore Information... - Julian Zinn Rakesh Verma
A Polynomial-time Algorithm for Uniqueness of Normal Forms of Linear Shallow Term Rewrite SystemsMore Information...
Organizers
General ChairPhokion G. Kolaitis Program ChairRajeev Alur Conference ChairMargus Veanes Publicity ChairStephan Kreutzer Nicole Schweikardt Workshops ChairPhilip J. Scott |
Program Committee:Luca Aceto (Reykjavik University, Iceland, and Aalborg University, Denmark); Rajeev Alur (University of Pennsylvania) (chair); Christel Baier (University of Bonn, Germany); Maria Luisa Bonet (Polytechnic University of Catalunya, Spai); Flavio Corradini (University of Camerino, Ital); Victor Dalmau (Universitat Pompeu Fabra, Spain); Thomas Eiter (TU Vienna, Austria); Kousha Etessami (University of Edinburgh, UK); Amy Felty (University of Ottawa, Canada); Cedric Fournet (Microsoft Research, UK); Patrice Godefroid (Bell Labs, USA); Jason Hickey (CalTech, USA); Radha Jagadeesan (DePaul University, USA); Leonid Libkin (University of Toronto, Canada); Patrick Lincoln (SRI, USA); Yoram Moses (Technion, Israel); George C. Necula (UC Berkeley, USA); Joël Ouaknine (Oxford University, UK); Davide Sangiorgi (University of Bologna, Italy); Mahesh Viswanatha (University of Illinois at Urbana-Champaign, USA); Thomas Wilke (University of Kiel, Germany) Organizing CommitteeSamson Abramsky; Rajeev Alur; Franz Baader; Andrei Z. Broder; Samuel R. Buss; Edmund M. Clarke; Amy Felty; Harold N. Gabow; Lauri Hella; Radha Jagadeesan; Alan Jeffrey; Phokion G. Kolaitis; Stephan Kreutzer; Johann A. Makowsky; John C. Mitchell; Mogens Nielsen; Prakash Panangaden; Femke van Raamsdonk; Nicole Schweikardt; Philip J. Scott; Margus Veanes; Andrei Voronkov Advisory BoardRobert L. Constable; Yuri Gurevich; Claude Kirchner; Dexter C. Kozen; Ursula Martin; Albert R. Meyer; Leszek Pacholski; Vaughan R. Pratt; Andre Scedrov; Dana S. Scott; Moshe Y. Vardi; Glynn Winskel |