FLoC on Wednesday, July 14th

See also the by session program.

AFM	FCS-PrivMod	HOR	ITP	LFMTP	LICS	PAAR	SAT	SMT	UNIF	WST
09:00‑10:00 Mark Hillebrand System Software Verification Using VCC		09:00‑10:00 Maribel Fernández (Invited Speaker) Closed nominal rewriting: properties and applications	09:00‑10:00 Benjamin C. Pierce (University of Pennsylvania) Proof Assistants as Teaching Assistants: A View from the Trenches		09:00‑10:00 Catuscia Palamidessi (INRIA and LIX, Ecole Polytechnique) Probabilistic Information Flow	09:00‑10:00 Jasmine Christian Blanchette (TU München) Invited talk: Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers	09:00‑10:00 Daniel Kroening A Primer on the Algorithmic Aspects of Satisfiability Modulo Theories	09:00‑10:00 SAT SMT Tutorial	09:00‑10:00 Claude Kirchner (INRIA Bordeaux-Sud-Ouest, France) Antipatterns: how to say what you don't want to match to	09:00‑10:00 Elvira Albert (Complutense University of Madrid) From Termination to Cost (in Object-Oriented Languages)
10:00‑10:30 Coffee break
10:30‑11:00 Cliff Jones, Gudmund Grov and Alan Bundy Ideas for a high-level proof strategy language 11:00‑11:30 Maria Teresa Llano Rodriguez, Gudmund Grov and Andrew Ireland Automatic Guidance for Refinement Based Formal Methods 11:30‑12:00 Aboubakr Achraf El Ghazi and Mana Taghdiri Analyzing Alloy Constraints using an SMT Solver: A Case Study	10:30‑11:00 Max Kanovich, Tajana Ban Kirigin, Vivek Nigam and Andre Scedrov Progressing Collaborative Systems 11:00‑11:30 Abdessamad IMINE, Zeeshan Ahmed and Michael Rusinowitch Safe and Efficient Strategies for Updating Firewall Policies 11:30‑12:00 Hakima Ould-Slimane, Mohamed Mejri and Kamel Adi Enforcing More Than Safety Properties by Program Rewriting: Algebraic Foundations 12:00‑12:30 Etienne Lozes Towards Information as Resource in Separation Logic	10:30‑11:00 Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson and Benoît Valiron Equivalence of algebraic λ-calculi 11:00‑11:30 Harald Zankl, Nao Hirokawa and Aart Middeldorp Uncurrying for Innermost Termination and Derivational Complexity 11:30‑12:00 Giulio Manzonetto and Paolo Tranquilli A Calculus of Coercions Proving the Strong Normalization of MLF 12:00‑12:30 Cynthia Kop (student talk) A new formalism for higher-order rewriting	10:30‑11:00 Matthieu Sozeau Equations: a dependent pattern-matching compiler 11:00‑11:30 Arthur Charguéraud The Optimal Fixed Point Combinator 11:30‑12:00 Thomas Braibant and Damien Pous An Efficient Coq Tactic for Deciding Kleene Algebras 12:00‑12:30 Peter Lammich and Andreas Lochbihler The Isabelle Collections Framework	10:25‑10:40 Marino Miculan Welcome 10:30‑11:00 Dan Licata and Robert Harper A Monadic Formalization of ML5 11:00‑11:30 Herman Geuvers, Robbert Krebbers, James McKinna and Freek Wiedijk Pure Type Systems without Explicit Contexts 11:30‑12:00 Florian Rabe Representing Isabelle in LF 12:00‑12:30 Andreas Abel and Brigitte Pientka Explicit substitutions for contextual type theory	10:30‑11:00 Magnus Johansson, Jesper Bengtson, Joachim Parrow and Björn Victor Weak Equivalences in Psi-calculi 11:00‑11:30 Massimo Bartoletti and Roberto Zunino A calculus of contracting processes 11:30‑12:00 Christian Eisentraut, Holger Hermanns and Lijun Zhang On Probabilistic Automata In Continuous Time 12:00‑12:30 Jean Goubault-Larrecq Omega-QRB-Domains and the Probabilistic Powerdomain	10:30‑11:00 Laura Meikle and Jacques Fleuriot Automation for Geometry in Interactive Theorem Provers 11:00‑11:30 Andrew Matusiwicz, Neil Murray and Erik Rosenthal Trie Based Subsumption and Improving the pi-Trie Algorithm 11:30‑12:00 Guido Fiorino Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus 12:00‑12:30 Thomas Bouton, Diego Caminha, David Deharbe and Pascal Fontaine GridTPT: a distributed platform for Theorem Prover Testing	10:30‑11:00 Vasco Manquinho, Ruben Martins and Inês Lynce Improving Unsatisfiability-based Algorithms for Boolean Optimization 11:00‑11:30 Denis Pankratov and Allan Borodin On the Relative Merits of Simple Local Search Methods for the Max Sat Problem 11:30‑11:50 Chu-Min LI, Felip Manya, Zhe Quan and Zhu Zhu Exact MinSAT Solving 11:50‑12:10 Rüdiger Ehlers Minimising Deterministic Büchi Automata Precisely using SAT Solving 12:10‑12:30 Gayathri Namasivayam and Mirosław Truszczynski Simple but Hard Mixed Horn Formulas	10:30‑11:30 Nikolai Tillman, Microsoft SMT-Solvers In (Tracing) Just-in-Time Compilers 11:30‑12:00 B. Paleo, S. Merz, P. Fontaine Exploring and Exploiting Algebraic and Graphical Properties of Resolution 12:00‑12:30 M. Bankovic and F. Maric Alldifferent Constraint Solver in SMT	10:30‑11:00 Sunil Kothari and James Caldwell A Machine Checked Model of Idempotent MGU Axioms For a List of Equational Constraints 11:00‑11:30 Franz Baader and Barbara Morawska SAT Encoding of Unification in EL 11:30‑12:00 Deepak Kapur, Andrew Marshall and Paliath Narendran Unification modulo a partial theory of exponentiation 12:00‑12:30 Conrad Rau and Manfred Schmidt-Schauß Towards Correctness of Program Transformations Through Unification and Critical Pair Computation	10:30‑11:00 Samir Genaim and Damiano Zanardini The Acyclicity Inference of COSTA 11:00‑11:30 Christophe Raffalli and Pierre Hyvernat Improvements on the "Size Change Termination Principle" in a functional language 11:30‑12:00 Thomas Stroeder, Jürgen Giesl and Peter Schneider-Kamp Termination Analysis of Logic Programs with Cut Using Dependency Triples 12:00‑12:30 Paolo Pilozzi and Danny De Schreye Scaling termination proofs by a characterisation of cycles in CHR
12:30‑14:00 Lunch
14:00‑15:00 Sam Owre and N. Shankar Probabilistic Reasoning with PCE	14:00‑15:00 Bart Jacobs (Technical University Eindhoven) Privacy and security issues in e-ticketing	14:00‑15:00 Silvia Ghilezan (Invited Speaker) Computational interpretations of logic	14:00‑14:30 Jasmin Christian Blanchette and Tobias Nipkow Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder 14:30‑15:00 Alexander Krauss and Andreas Schropp A Mechanized Translation from Higher-Order Logic to Set Theory	14:00‑14:30 Anders Schack-Nielsen and Carsten Schuermann Pattern Unification for the Lambda Calculus with Linear and Affine Types 14:30‑15:00 Maribel Fernandez and Murdoch Gabbay Closed nominal rewriting and efficiently computable nominal algebra equality	14:00‑15:00 Vincent Danos (The University of Edinburgh and CNRS) Abstracting the ODE semantics of rule-based models: exact and automatic model reduction	14:00‑15:00 Andrei Voronkov (University of Manchester) Invited Talk: Vampire: the Fresh Blood	14:00‑14:20 Miquel Bofill, Josep Suy and Mateu Villaret A system for solving constraint satisfaction problems with SMT 14:20‑14:50 J. Christ, J. Hoenicke (SMT'10) Instantiation-Based Interpolation for Quantified Formulae	14:00‑14:20 Miquel Bofill, Josep Suy and Mateu Villaret (SAT'10) A system for solving constraint satisfaction problems with SMT 14:20‑14:50 J. Christ, J. Hoenicke Instantiation-Based Interpolation for Quantified Formulae	14:00‑15:00 Christian Urban (Technical University Munich, Germany) Nominal Unification - Hitting a Sweet Spot	14:00‑14:30 Dean Voets and Danny De Schreye Non-termination analysis of Logic Programs using Types 14:30‑15:00 Naoki Nishida, Masahiko Sakai and Tatsuya Hattori On Disproving Termination of Constrained Term Rewriting Systems
15:00‑15:30 Coffee break
15:30‑16:00 Meng Wenrui Assume-Guarantee for Reachability 16:00‑17:00 Discussion	15:30‑16:00 Jonathan Millen and John Ramsdell Annotated sequence diagrams 16:00‑16:30 Ralf Kuesters, Henning Schnoor and Tomasz Truderung A Formal Definition of Online Abuse-freeness 16:30‑17:00 SARR Augustin P., Elbaz--Vincent Philippe and Bajard Jean--Claude Enhanced Security and Efficiency for Authenticated Key Agreement	15:30‑16:00 Thibaut Balabonski On the Implementation of Dynamic Patterns 16:00‑16:30 Kristoffer Rose Higher-order Rewriting for Executable Compiler Specifications 16:30‑17:00 Ariel Mendelzon, Alejandro Ríos and Beta Ziliani Swapping: a natural bridge between named and indexed explicit substitution calculi 17:00‑17:30 Delia Kesner, Carlos Lombardi and Alejandro Ríos Standardisation for constructor based pattern calculi	15:30‑16:00 Chantal Keller and Benjamin Werner Importing HOL-Light into Coq 16:00‑16:30 Sascha Böhme and Tjark Weber Fast LCF-Style Proof Reconstruction for Z3 16:30‑17:00 Tjark Weber Validating QBF Invalidity in HOL4	15:30‑16:00 John Boyland Generating Bijections between HOAS and the Natural Numbers 16:00‑17:00 Chung-chieh Shan (Rutgers, The State University of New Jersey) Typed metaprogramming with effects 17:00‑18:00 Frank Pfenning (Carnegie Mellon University) The Practice and Promise of Substructural Frameworks 18:00‑18:10 Marino Miculan Closing	15:30‑16:00 Cosimo Laneve and Antonio Vitale The Expressive Power of Synchronizations 16:00‑16:30 Sam Staton and Glynn Winskel On the expressivity of symmetry in event structures 16:30‑17:00 Thomas Ehrhard A finiteness structure on resource terms 17:15‑17:45 Samson Abramsky Coalgebras, Chu Spaces, and Representations of Physical Systems 17:45‑18:15 Stefan Milius A Sound and Complete Calculus for finite Stream Circuits 18:15‑18:20 Closing	15:30‑15:55 Djihed Afifi, David Rydeheard and Howard Barringer Automated Reasoning in the Simulation of Evolvable Systems 15:55‑16:20 Han-Hing Dang and Peter Höfner Automated Higher-order Reasoning in Quantales 16:20‑16:45 Jens Otten and Geoff Sutcliffe Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi 16:45‑17:10 Christoph Benzmueller and Adam Pease Progress in Automating Higher-Order Ontology Reasoning 17:10‑17:35 Ullrich Hustadt and Renate A. Schmidt A Comparison of Solvers for Propositional Dynamic Logic	15:30‑16:00 Claudia Peschiera, Luca Pulina, Armando Tacchella, Uwe Bubeck, Oliver Kullmann and Ines Lynce The Seventh QBF Solvers Evaluation (QBFEVAL'10) 16:00‑16:30 Competition 16:30‑17:00 Competition 17:00‑17:30 Competition	15:30‑16:00 C. Barrett, A. Stump, C. Tinelli The SMT-LIB Standard – Version 2.0	15:30‑16:00 Christophe François Olivier Calvès Nominal Theory as an Extension of First-Order Theory 16:00‑16:30 Sergiu Bursuc and Cristian Prisacariu Unification and matching in separable theories 16:30‑17:00 Zhiqiang Liu and Christopher Lynch Efficient XOR Unification 17:00‑17:30 Paliath Narendran, Andrew Marshall and Bibhu Mahapatra On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided Distributivity	15:30‑16:00 Friedrich Neurauter and Aart Middeldorp Polynomial Termination over N and R does not imply Polynomial Termination over Q 16:00‑16:30 Michael Codish, Carsten Fuhs, Jürgen Giesl and Peter Schneider-Kamp Lazy abstraction for size-change termination 16:30‑17:00 Dieter Hofbauer and Johannes Waldmann Match-Bounds for Relative Termination