FLoC on Tuesday, July 20th

See also the by session program.

ASPOCP	CHR	EC2	EMSQMS	FCC	SVARM	UniDL	VERIFY	WG17
09:00‑10:00 Torsten Schaub ASP Solving and Other Computing Paradigms	09:00‑10:00 Mark Proctor (JBoss) Drools Business Logic integration Platform Tutorial	09:00‑10:00 Keshav Pingali (UT Austin) Invited talk: Parallel Programming Needs New Foundations	09:00‑10:00 Joe Hurd Evaluation Opportunities in Mechanized Theories	09:00‑10:00 Dennis Hofheinz Public key encryption schemes with special properties	09:00‑09:30 Ras Bodik Next Steps in Partial-Program Synthesis 09:30‑10:00 Kim Larsen Controller Synthesis from Timed Game Automata – from Theory to Practice	09:00‑09:05 Welcoming introduction 09:05‑10:00 Ralf Möller (University of Hamburg-Harburg) Invited talk: A Probabilistic Abduction Engine for Media Interpretation based on Ontologies	08:50‑09:00 Invited Talk 09:00‑10:00 Cliff Jones (Newcastle University, UK) Abstractions Before Proofs	09:00‑10:00 Opening, Introductions.Approval of the Minutes of the Pasdena meeting.Approval of the Agenda.
10:00‑10:30 Coffee break
10:30‑11:00 Christian Drescher, Oana Tifrea and Toby Walsh Symmetry-breaking Answer Set Solving 11:00‑11:30 Marcello Balduccini Improving DPLL Solver Performance with Domain-Specific Heuristics: the ASP Case 11:30‑12:00 Martin Gebser, Orkunt Sabuncu and Torsten Schaub An Incremental Answer Set Programming Based System for Finite Model Computation: Preliminary Report 12:00‑12:30 Mario Alviano and Wolfgang Faber Dynamic Magic Sets for Super-Consistent Answer Set Programs	10:30‑11:15 Thom Frühwirth (University of Ulm) Constraint Handling Rules Tutorial 11:15‑11:40 Johannes Langbein, Frank Raiser and Thom Fruehwirth A State Equivalence and Confluence Checker for CHR 11:40‑12:05 Peter Van Weert Join Ordering for Constraint Handling Rules: Putting Theory into Practice 12:05‑12:30 Matt Lilley (SecuritEase) SWI Forms - Bringing logic to UI development	10:30‑10:50 Thomas Henzinger, Anmol Tomar, Vasu Singh, Thomas Wies and Damien Zufferey (EC)^2 in EC2 10:50‑11:10 Azadeh Farzan, Madhusudan Parthasarathy and Francesco Sorrentino PENELOPE: Weaving Threads to Violate Atomicity 11:10‑11:30 Khilan Gudka and Susan Eisenbach Fast Multi-Level Locks for Java 11:30‑12:30 Challenge Problems for Concurrency Verification.	10:30‑11:00 Robert Brummayer, Aaron Stump and Duckki Oe Exploring Predictability of SAT/SMT Solvers 11:00‑11:30 Claudia Peschiera, Luca Pulina and Armando Tacchella Designing a solver competition: the QBFEVAL'10 case study 11:30‑12:00 Mladen Nikolic Statistical Methodology for Comparison of SAT Solvers 12:00‑12:30 Christoph Benzmueller and Marvin Schiller Adaptive Proofs supported by Metadeduction	10:30‑11:00 Catherine Meadows and Dusko Pavlovic A Framework for Extending Algebraic to Computational Reasoning in Cryptographic Protocol Analysis 11:00‑11:30 Dominique Unruh Computational Soundness of Hash Functions 11:30‑12:00 Steve Kremer, Hubert Comon-Lundh and Joe-Kai Tsay Modular Soundness Proofs via Deduction Games (work in progress) 12:00‑12:30 Ralf Kuesters and Max Tuengerthal Ideal Key Derivation and Encryption in Simulation-based Security	10:30‑11:00 Alexander Rabinovich Extensions of the Church synthesis Problem 11:00‑11:30 Bernd Finkbeiner Bounded Synthesis 11:30‑12:00 Georg Hofferek and Roderick Bloem Controller Synthesis Using Uninterpreted Functions 12:00‑12:30 Barbara Jobstmann Quantitative Verification and Synthesis	10:30‑10:55 Pavel Klinov and Bijan Parsia Relationships between Probabilistic Description and First-Order Logics 10:55‑11:20 Paulo Santos, Fabio Cozman, Valquiria Fenelon Pereira and Britta Hummel Probabilistic Logic Encoding of Spatial Domains 11:20‑11:45 Oliver Gries and Ralf Möller Gibbs Sampling in Probabilistic Description Logics with Deterministic Dependencies 11:45‑12:10 Anni-Yasmin Turhan and Rafael Peñaloza Towards Approximative Most Specific Concepts by Completion for EL with Subjective Probabilities 12:10‑12:35 Rommel Carvalho, Kathryn Laskey and Paulo Costa Compatibility Formalization Between PR-OWL and OWL	10:30‑11:10 Angelo Brillout, Daniel Kroening, Philipp Ruemmer and Thomas Wahl Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays 11:10‑11:50 Shuling Wang and Xu Wang Proving Four-Slot Algorithm Using Ownership Transfer 11:50‑12:30 Michael von Tessin Towards High-Assurance Multiprocessor Virtualisation	10:30‑12:30 Globals Japanese Contribution on Globals. Editorial Review, Katsuhiko Nakamura
12:30‑14:00 Lunch
14:00‑14:30 Dov Gabbay, David Pearce and Agustin Valverde Interpolation in Equilibrium Logic and Answer Set Programming: the Propositional Case 14:30‑15:00 Pedro Cabalar A Logical Characterisation of Ordered Disjunction	14:00‑14:25 Henning Christiansen, Christian Theil Have, Ole Torp Lassen and Matthieu Petit The Viterbi Algorithm expressed in Constraint Handling Rules 14:25‑14:40 Jon Sneyers (K.U.Leuven) CHRiSM Introduction 14:40‑15:00 Jon Sneyers Result-directed CHR Execution	14:00‑15:00 Tim Harris (Microsoft (Cambridge)) Invited Talk: Programming models for the Barrelfish multi-kernel operating system	14:00‑14:30 Morgan Deters The SMT Execution Service: Features, Fairness, and the Future 14:30‑15:00 Geoff Sutcliffe, Cynthia Chang, Li Ding, Deborah McGuinness and Paulo Pinheiro da Silva Different Proofs are Good Proofs	14:00‑14:30 Gilles Barthe, Benjamin Gregoire, Daniel Hedin, Sylvain Heraud and Santiago Zanella Béguelin Towards automating code-based game-based cryptographic proofs 14:30‑15:00 Bruno Blanchet and David Pointcheval The computational and decisional Diffie-Hellman assumptions in CryptoVerif	14:00‑15:00 Natarajan Shankar Inference Architectures for Satisfiability Modulo Theories	14:00‑14:25 Pavel Klinov and Bijan Parsia Pronto: A Practical Probabilistic Description Logic Reasoner 14:25‑14:50 Nicola Vitucci, Mario Arrigoni Neri and Giuseppina Gini Using f-SHIN to Represent Objects: An Aid to Visual Grasping	14:00‑15:00 Véronique Cortier (LORIA INRIA-Lorraine, France) Verification of Security Protocols	14:00‑15:00 Missing Predicates. Ulrich Neumerkel
15:00‑15:30 Coffee break
15:30‑16:00 Stefania Costantini and Alessio Paolucci Towards Translating Natural Language Sentences into ASP 16:00‑16:30 Cristina Feier and Stijn Heymans An Optimization for Reasoning with Forest Logic Programs 16:30‑17:00 Yves Moinard Using ASP with Recent Extensions for Causal Explanations	15:30‑15:55 Ralf Gerlich Generic and Extensible Automatic Test Data Generation for Safety Critical Software with CHR 15:55‑16:20 Florian Geiselhart, Frank Raiser, Jon Sneyers and Thom Fruehwirth MTSeq - multi-touch-enabled music generation and manipulation based on CHR 16:20‑16:45 Ayman Adel Abdelsamie Abdelaal, Frank Raiser, Thom Frühwirth, and Roland Stelzer Long-term routing for autonomous sail boats with CHR 16:45‑17:00 Peter Van Weert Conclusions	15:30‑15:50 Konrad Siek and Paweł Wojciechowski Statically Computing Upper Bounds on Object Calls for Pessimistic Concurrency Control 15:50‑16:10 Chao Wang, Malay Ganai and Aarti Gupta Symbolic Predictive Analysis to Expose Concurrency Errors at Runtime 16:10‑16:30 Andras Salamon and Vashti Galpin Performance loss between concept and keyboard 16:30‑17:00 Q-and-A session with all the speakers	15:30‑16:15 EMS panel on solver competitions and community infrastructure (shared with SVARM) 16:15‑17:00 QMS facilitated discussion on quality metrics for solutions	15:30‑16:00 Gergei Bana, Koji Hasebe and Mitsuhiro Okada Secrecy-Oriended, Computationally Sound First-Order Logical Analysis of Cryptographic Protocols 16:00‑16:30 Pedro Adao and Gergei Bana Logical Proofs of Authentication Protocols and Type-Flaw Attacks	15:30‑16:15 Panel joint with EMSQMS 16:30‑17:00 Armin Biere and Florian Lonsing Extending the BTOR Language 17:00‑17:30 Tobias Nipkow Automatic proof and disproof in Isabelle 17:30‑18:00 Action IC0901 Management Committee Meeting	15:30‑17:00 Demos & Discussion	15:30‑16:10 Mark Bickford Automated Proof of Authentication Protocols in a Logic of Events 16:10‑16:50 Bernhard Beckert, Daniel Bruns and Sarah Grebing Mind the Gap: Formal Verification and the Common Criteria 19:00‑22:00 Workshop Dinner (tentative)	15:30‑17:00 DCGs. Klaus Daessler