FLoC on Wednesday, July 21st

See also the by session program.

ASA	EC2	ICLP-DC	SVARM	VERIFY	WCB	WG17	WING
09:15‑09:30 Opening remarks 09:30‑10:00 Robert Watson and Jonathan Anderson Connecting the Dot-Dots: Model Checking Concurrency in a Security API	09:00‑10:00 Bill Gropp (UIUC) Invited talk: Challenges in Using the Message Passing Interface in Multicore and Heterogeneous Systems	09:00‑09:20 Romain Demeyer Program Analysis to Support Concurrent Programming in Declarative Languages 09:20‑09:40 Thierry Martinez Design and Implementation of a Concurrent Logic Programming Language with Linear Logic Constraints 09:40‑10:00 Andrés A. Aristizábal Bisimilarity in Concurrent Constraint Programming	09:00‑10:00 Bernhard Beckert Formal Verification of System Software	09:00‑10:00 André Platzer (Carnegie Mellon University, USA) Real Analysis for Complex Systems	09:00‑10:00 Alexander Bockmayr Constraint-based modeling in systems biology	09:00‑10:00 Globals Final Editorial Review	09:00‑10:00 Helmut Seidl Abstract Interpretation Meets Mathematical Optimization
10:00‑10:30 Coffee break
10:30‑11:00 Graham Steel Abstractions for Verifying Key Management APIs 11:00‑11:30 Sibylle Froeschle and Nils Sommer When is a PKCS#11 configuration secure? 11:30‑12:00 Matteo Bortolozzo, Matteo Centenaro, Riccardo Focardi and Graham Steel CryptokiX: a cryptographic software token with security fixes 12:00‑12:30 François Dupressoir, Andrew D. Gordon and Jan Jürjens Verifying Authentication Properties of C Security Protocol Code Using General Verifiers	10:30‑10:50 Alan Humphrey, Christopher Derrick, Beth Tibbitts, Anh Vo, Sarvani Vakkalanka, Ganesh Gopalakrishnan, Bronis de Supinski, Martin Schulz and Greg Bronevetsky Verification for Portability, Scalability, and Grokkability 10:50‑11:10 Rajesh Karmani and P Madhusudan A Contract Language for Race-Freedom 11:10‑11:30 Ariel Cohen, Kedar Namjoshi, Yaniv Sa'ar, Lenore Zuck and Katya Kisyova Model Checking in Bits and Pieces 11:30‑12:00 Concurrency Education	10:30‑10:50 Mario Alviano Dynamic Magic Sets for Disjunctive Datalog Programs 10:50‑11:10 Fabio Parisini Local Branching in a Constraint Programming Framework 11:10‑11:30 Céline Dandois Program Analysis for Code Duplication in Logic Programs 11:30‑11:50 Zachary Snow Realizing the Dependently Typed Lambda Calculus 11:50‑12:10 Abdulla Alqaddoumi Towards a Parallel Virtual Machine for Functional Logic Programming 12:10‑12:30 Niels Pahlavi Higher-order Logic Learning and λProgol	10:20‑10:40 Peter Schneider-Kamp Towards Complexity and Termination Analysis of Transition Systems 10:40‑11:00 Peter Habermehl, Lukas Holik, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar A Proposal of a New Automata-based Representation of Heaps 11:00‑11:20 Marius Bozga, Radu Iosif, Filip Konecny and Tomas Vojnar FLATA: Towards a Toolset for manipulation and analysis of counter automata 11:20‑11:30 Mini Break of 10 Minutes 11:30‑11:50 Stefan Ratschan Verification of Mixed Discrete-Continuous Systems 11:50‑12:10 Alejandro Sanchez and Cesar Sanchez Towards Temporal Verification of Concurrent Data-structures: In Need for Sophisticated Decision Procedures 12:10‑12:30 Hossein Hojjat, Viktor Kuncak, Ruzica Piskac and Philippe Suter Vepar: A Framework for Automated Reasoning	10:30‑11:10 Joe Hurd Composable Packages for Higher Order Logic Theories 11:10‑11:50 Andrei Lapets User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier 11:50‑12:30 Alessandro Carioni, Silvio Ghilardi and Silvio Ranise MCMT in the Land of Parametrized Timed Automata	10:30‑11:00 Pedro Barahona Minimizing enzymes to diferenciate between species 11:00‑11:30 James Cussens Maximum likelihood pedigree reconstruction using integer programming 11:30‑12:00 Aurélie Favier, Jean-Michel Elsen, Simon de Givry and Andrés Legarra Optimal haplotype reconstruction in half-sib families 12:00‑12:30 Alessandro Dal Palu, Mathias Möhl and Sebastian Will Alignnment of RNA with Structures of Unlimited Complexity	10:30‑12:30 Missing Predicates Final Editorial review	10:30‑11:00 Stephane Gaubert, Ricardo Katz and Sergei Sergeev Tropical linear programming and parametric mean payoff games 11:00‑11:22 Michael Franssen Cocktail II 11:22‑11:44 Igor Konnov CheAPS: a Checker of Asynchronous Parameterized Systems 11:44‑12:06 Ewen Maclean, Andrew Ireland and Gudmund Grov Synthesising Functional Invariants in Separation Logic 12:06‑12:28 Florian Zuleger and Moritz Sinn LOOPUS - A Tool for Computing Loop Bounds for C Programs
12:30‑14:00 Lunch
14:00‑14:30 Ronald Toegl Construction of a Trusted Virtual Security Module 14:30‑15:00 Mike Bond and George French Hidden Semantics: why? how? and what to do?	14:00‑15:00 Miriam Leeser (Northeastern University) Invited talk: GPU programming: bugs, pitfalls and the importance of correctness in biomedical and scientific applications	14:00‑14:20 Christian Drescher Constraint Answer Set Programming Systems 14:20‑14:40 Sarah Alice Gaggl Towards a General Argumentation System based on Answer-Set Programming 14:40‑15:00 Jakob Zwirchmayr Cutting-Edge Timing Analysis Techniques	14:00‑14:20 Paul Jackson and Grant Passmore Verification of Mixed Discrete-Continuous Systems 14:20‑14:40 Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic 14:40‑15:00 Timothy Nelson, Dougherty Daniel, Kathi Fisler and Shriram Krishnamurthi On the Finite Model Property in Order-Sorted Logic	14:00‑14:30 13:50 Daniel Wasserrab and Denis Lohner Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing 14:30‑15:00 Enrico Giunchiglia , Massimo Narizzano , Gabriele Palma and Alessandra Puddu Automatic generation of high quality test sets via CBMC	14:00‑14:30 Martin Mann and Alessandro Dal Palu' Lattice model refinement of protein structures 14:30‑15:00 Alejandro Arbelaez, Youssef Hamadi and Michele Sebag Building Portfolios for the Protein Structure Prediction Problem	14:00‑15:00 DCGs Final Editorial review	14:00‑15:00 Sumit Gulwani Methods for Loop Invariant Generation
15:00‑15:30 Coffee break
15:30‑17:00 Andrew Gordon, Reiner Hähnle, Cliff Jones, Mark Ryan, Riccardo Focardi, Johann Schumann Panel Session; Formal Methods as/in/for industry	15:30‑15:50 Marius Bozga and Emmanuel Sifakis Issues on Memory Management for Component-Based Models 15:50‑16:10 Vasu Singh Memory Model Relaxations to Boost TM Performance 16:10‑16:30 Guodong Li and Ganesh Gopalakrishnan PUG: A symbolic verification and test generation tool for GPU programs 16:30‑17:00 Q-and-A session with all the speakers	15:30‑15:50 Mauricio Toro-bermudez Structured Interactive Musical Scores 15:50‑16:10 Neda Saeedloei Logic Programming Foundations of Cyber-Physical Systems 16:10‑16:30 Hugo A. López Models for Trustworthy Services and Process Oriented Systems	15:20‑15:40 Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic and Jovanka Pantovic Types for dynamic web data with RBAC 15:40‑16:00 Predrag Janicic and Filip Maric Uniform reduction to SMT 16:00‑16:20 Maria Paola Bonacina and Moa Johansson Advances in rewrite-based decision procedures 16:20‑17:00 Closing Discussions	15:30‑17:00 Riccardo Focardi, Andrew Gordon, Reiner Hähnle, Cliff Jones, Mark Ryan, Johann Schumann Panel Discussion: Formal Methods for/in/as Industry	15:30‑16:00 Corinna Heldt and Alexander Bockmayr Geometric Constraints for the Phase Problem in X-Ray Crystallography 16:00‑16:30 Takehide Soh and Katsumi Inoue Finding Minimal Reaction Sets in Large Metabolic Pathways 16:30‑17:00 Luca Bortolussi and Alberto Policriti Perspectives on Constraints, Process Algebras, and Hybrid Systems	15:30‑17:00 Resolutions.	15:30‑16:00 Matthias Kuntz, Stefan Leue and Christoph Scheben Extending Non-Termination Proof Techniques to Communicating Asynchronous Concurrent Programs 16:00‑16:22 Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich and Christoph M. Wintersteiger Loopfrog — loop summarization for static analysis 16:22‑16:44 Vlad Volkov, Alexander Letichevsky, Alexander Kolchin, Oleksandr Letychevskyy jr., Stepan Potiyenko and Thomas Weigert Formal Requirements Capturing using VRS system 16:44‑17:06 Alexei Lisitsa Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol 17:06‑17:28 Radu Iosif, Marius Bozga, Filip Konecny and Tomas Vojnar Tool Demonstration of the FLATA Counter Automata Toolset