FLoC on Saturday, July 17th

See also the by session program.

CAV	CSF	ICLP	IJCAR
09:00‑10:00 Pasquale Malacaria Quantitative Information Flow: from Theory to Practice?	09:00‑09:05 Andrew Myers Conference welcome 09:05‑10:00 Vitaly Shmatikov (University of Texas, Austin) The end of anonymity, the beginning of privacy	09:00‑10:00 Francois Fages (INRIA Paris-Rocquencourt) A Logical Paradigm for Systems Biology	09:00‑10:00 Johan van Benthem (Stanford University and University of Amsterdam) Logic between Expressivity and Complexity
10:00‑10:30 Coffee break
10:30‑10:55 Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems 10:55‑11:20 Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns and Ernst Moritz Hahn Safety Verification for Probabilistic Hybrid Systems 11:20‑11:45 Khalil Ghorbal, Eric Goubault and Putot Sylvie A Logical Product Approach to Zonotope Intersection 11:45‑12:10 Radu Iosif, Marius Bozga and Filip Konecny Fast Acceleration of Ultimately Periodic Relations 12:10‑12:35 Luca Pulina and Armando Tacchella An Abstraction-Refinement Approach to Verification of Artificial Neural Networks	10:30‑11:00 Boris Köpf and Andrey Rybalchenko Approximation and randomization for quantitative information-flow analysis 11:00‑11:30 Hirotoshi Yasuoka and Tachio Terauchi Quantitative information flow - verification hardness and possibilities 11:30‑12:00 Michael Clarkson and Fred Schneider Quantification of integrity 12:00‑12:30 Boris Köpf and Geoffrey Smith Vulnerability bounds and leakage resilience of blinded cryptography under timing attacks	10:30‑11:00 Christian Drescher and Toby Walsh A Translational Approach to Constraint Answer Set Solving 11:00‑11:30 Sabrina Baselice and Piero Bonatti Decidable subclasses of finitary programs 11:30‑12:00 Mario Alviano, Wolfgang Faber and Nicola Leone, Disjunctive ASP with Functions: Decidable Queries and Effective Computation 12:00‑12:30 Johannes Oetsch, Joerg Puehrer and Hans Tompits Catching the Ouroboros: On Debugging Non-ground Answer-Set Programs	10:30‑11:00 Ali Ayad and Claude Marché Multi-Prover Verification of Floating-Point Programs 11:00‑11:15 Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport and Stephan Merz Verifying Safety Properties With the TLA+ Proof System 11:15‑11:30 Ruzica Piskac and Viktor Kuncak MUNCH - Automated Reasoner for Sets and Multisets 11:30‑12:00 Elena Sherman, Brady J. Garvin and Matthew B. Dwyer A Slice-based Decision Procedure for Type-based Partial Orders 12:00‑12:30 Viorica Sofronie-Stokkermans Hierarchical reasoning for the verification of parametric systems
12:30‑14:00 Lunch
14:00‑14:25 Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell Fences in Weak Memory Models 14:25‑14:50 Sela Mador-Haim, Rajeev Alur and Milo M. K. Martin Generating Litmus Tests for Contrasting Memory Consistency Models	14:00‑14:30 Mathilde Arnaud, Véronique Cortier and Stephanie Delaune Modeling and verifying ad hoc routing protocols 14:30‑15:00 Mayla Bruso, Konstantinos Chatzikokolakis and Jerry den Hartog Formal verification of privacy for RFID systems	14:00‑14:12 Selen Basol, Ozan Erdem, Michael Fink and Giovambattista Ianni HEX Programs with Action Atoms 14:12‑14:24 Christoph Wernhard Circumscription and Projection as Primitives of Logic Programming 14:24‑14:36 Luis Moniz Pereira and Alexandre Miguel Pinto Tight Semantics for Logic Programs 14:36‑14:48 Joseph Near From Relational Specifications to Logic Programs 14:48‑15:00 Stefan Brass Implementation Alternatives for Bottom-Up Evaluation	14:00‑14:15 Krystof Hoder, Laura Kovacs and Andrei Voronkov Symbol Elimination and Interpolation in Vampire 14:15‑14:30 Konstantin Korovin and Christoph Sticksel iProver-Eq: An Instantiation-based Theorem Prover with Equality 14:30‑15:00 Hans de Nivelle Classical Logic with Partial Functions
15:00‑15:30 Coffee break
15:30‑15:55 Aditya Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen and Thomas Reps Directed Proof Generation for Machine Code 15:55‑16:20 Christopher Conway and Clark Barrett Verifying Low-Level Implementations of High-Level Datatypes 16:20‑16:45 Satrajit Chatterjee and Michael Kishinevsky Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics 16:45‑17:10 Juncao Li, Fei Xie, Thomas Ball and Vladimir Levin Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification 17:15‑17:30 Stefan Blom, Jaco van de Pol and Michael Weber LTSMIN: Distributed and Symbolic Reachability 17:30‑17:45 Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider and David R. Piegdon libalf: the Automata Learning Framework 18:00‑19:00 Business Meeting	15:30‑16:00 Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk and Bogdan Warinschi Robustness guarantees for anonymity 16:00‑16:30 Myrto Arapinis, Tom Chothia, Eike Ritter and Mark Ryan Analysing unlinkability and anonymity using the applied pi-calculus 16:30‑17:00 Ralf Kuesters, Tomasz Truderung and Andreas Vogt A game-based definition of coercion-resistance and its applications 17:00‑18:00 List of talks at http://people.seas.harvard.edu/~chong/csf2010-5min/	15:30‑16:30 ALP community meeting 16:30‑18:00 The 2010 Prolog programming contest	15:30‑15:45 Christoph Beierle, Marc Finthammer, Gabriele Kern-Isberner and Matthias Thimm Automated Reasoning for Relational Probabilistic Knowledge Representation 15:45‑16:15 Rajeev Goré and Florian Widmann Optimal Tableaux for Propositional Dynamic Logic with Converse 16:15‑16:45 Mark Kaminski and Gert Smolka Terminating Tableaux for Hybrid Logic with Eventualities 16:45‑17:00 Marta Cialdea Mayer and Serenella Cerrito Herod and Pilate: two tableau provers for basic hybrid logic 17:10‑17:50 CADE Business Meeting 17:50‑18:30 Tableaux Business Meeting