ABOUT FLOC
HOME About FLoC Sponsors Mailing list Contact
PARTICIPATION
Registration Accommodation Student travel support US-based Student travel support Visa information Cancellation Policy Local information Reimbursement forms (new!)
MEETINGS
CAV CSF ICLP IJCAR ITP LICS RTA SAT Workshops (alpha.) Workshops (by conf.) Affiliated Events
PROGRAM
FLoC at a glance Meeting by meeting Day by day Room assignment Invited talks Accepted papers Social events FLoC Brochure (PDF)
!! LAST MINUTE NEWS !! !! ROOM CHANGES !!
ORGANIZATION
Steering Committee Programme Committee Organising Committee
MISCELLANEOUS
Call for Workshops

FLoC on Thursday, July 15th

previous day next day See also the by session program.
CAV
CICLOPS-WLPE
CLoDeM
FCS-PrivMod
HWVW
LAM
LaSh
LfSA
MLPA
NSV
PAR
PSTT
SMT
UITP
WST
09:00‑10:00
Robert Brayton
ABC: An Academic Industrial-Strength Verification Tool
09:00‑10:00
Naoyuki Tamura (Kobe University, Japan)
Solving Constraint Satisfaction Problems by a SAT Solver
09:00‑10:00
Moshe Vardi (Rice University, US)
Symbolic Techniques in Propositional Satisfiability Solving
09:00‑10:00
Hubert Comon-Lundh (CNRS & ENS de Cachan)
Symbolic and computational proofs of security
09:00‑10:00
Sharad Malik (Princeton University, USA)
Invited talk: Managing State Explosion through Runtime Verification
09:00‑10:00
Frank Pfenning (Carnegie Mellon University)
Possession as Linear Knowledge
09:00‑10:00
Ilkka Niemela (Aalto University)
Integrating Answer Set Programming and Satisfiability modulo Theories
09:00‑10:00
Thomas A. Henzinger (IST Austria)
The Quantitative Agenda in System Analysis
09:00‑10:00
Ulf Norell (Chalmers University)
Modules and records in Agda
08:25‑08:30
Opening
08:30‑09:30
Sylvie Boldo (INRIA Saclay)
Formal verification of numerical programs: from C annotated programs to Coq proofs
09:30‑10:00
Pieter Collins, Milad Niqui and Nathalie Revol
A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq (Extended abstract)
09:00‑10:00
Alexander Krauss
Recursive Definitions of Monadic Functions
09:00‑10:00
Silvio Ghilardi, U. Milano
SMT model checking for array-based systems
09:30‑10:00
John Slaney
Visualising Reasoning: What ATP can learn from CP
09:00‑09:30
Christian Sternagel and René Thiemann
Certification extends Termination Techniques
09:30‑10:00
Madalina Erascu and Tudor Jebelean
A Purely Logical Approach to Program Termination
10:00‑10:30
Coffee break
10:30‑11:00
Tutorial 1 continued
11:00‑12:30
Ken McMillan
Software Model Checking (TBC)
10:30‑11:00
Peter Biener, François Degrave and Wim Vanhoof
A Test Automation Framework for Mercury
11:00‑11:30
Petra Hofstedt
Realizing evaluation strategies by hierarchical graph rewriting
11:30‑12:00
Nicos Angelopoulos and Paul Taylor
An extensible web interface for databases and its application to storing biochemical data
12:00‑12:30
Paulo Moura
Meta-Predicate Semantics
10:30‑11:00
Oliver Friedmann and Markus Latte
Decision Procedures for CTL*
11:00‑11:30
Rajeev Gore and Florian Widmann
An Experimental Comparison of Theorem Provers for CTL
11:30‑12:30
Jerome Leroux (Labri Bordeaux, France)
Presburger Automata
10:30‑11:00
Karthikeyan Bhargavan, Cédric Fournet and Nataliya Guts
Pre- and Post-conditions for Security Typechecking
11:00‑11:30
Morten Dahl and Hans Hüttel
Don't Let The Opponents Grind You Down
11:30‑12:00
Radha Jagadeesan, Alan Jeffrey, Corin Pitcher and James Riely
Confidential Safety via Correspondence Assertions
12:00‑12:30
Sreekanth Malladi
Protocol independence through disjoint encryption under Exclusive-OR
10:30‑11:00
Matthias Raffelsieper and Mohammadreza Mousavi
Efficient Verification of Verilog Cell Libraries
11:00‑11:30
Yongjian Li, William Hung and Xiaoyu Song
Automatically Exploring Structural Symmetry in Symbolic Trajectory Evaluation
11:30‑12:00
Divjyot Sethi, Yogesh Mahajan and Sharad Malik
Specification and Encoding of Transaction Interaction Properties
12:00‑12:30
Malay Ganai and Weihong Li
Bang for the Buck: Improvising and Scheduling Verification Engines for Effective Resource Utilization
10:30‑11:00
Thierry Sans and Iliano Cervesato
QWeSST for Type-Safe Web Programming
11:00‑11:30
Vivek Nigam, Limin Jia, Anduo Wang, Boon Thau Loo and Andre Scedrov
An Operational Semantics for Network Datalog
11:30‑12:00
Andrea Bracciali, Jane Hillston, Diego Latella and Mieke Massink
Reconciling Population and Agent Models for Crowd Dynamics
12:00‑12:30
Prakash Panangaden and Mehrnoosh Sadrzadeh
Towards a logic for reasoning about learning in a changing world
10:30‑10:49
Shahab Tasharrofi and Eugenia Ternovska
Built-in Arithmetic in Knowledge Representation Languages
10:49‑11:08
Emanuele Di Rosa and Enrico Giunchiglia
Evaluating approaches for solving Satisfiability problems with Preferences
11:08‑11:27
Sid Mijnders, Boris de Wilde and Marijn J.H. Heule
Symbiosis of Search and Heuristics for Random 3-SAT
11:27‑11:33
Mini-break
11:33‑11:52
Antti Hyvärinen, Tommi Junttila and Ilkka Niemelä
Partitioning SAT Instances for Distributed Solving
11:52‑12:11
Broes De Cat and Marc Denecker
DPLL(Agg): an efficient SMT module for aggregates.
12:11‑12:30
Daniel Le Berre and Pascal Rapicault
Dependency Management for the Eclipse Ecosystem: An Update
10:30‑11:00
Christian Engel and Peter Schmitt
A Formalization of the RTSJ Scoped Memory Model in Dynamic Logic
11:00‑11:30
Alessandro Cimatti, Marco Roveri and Stefano Tonetta
Requirements Validation for Hybrid Systems
11:30‑12:00
Hongyang Qu, Marta Kwiatkowska, Gethin Norman and David Parker
Assume-Guarantee Verification for Probabilistic Systems
12:00‑12:30
Will Harwood, John Clark and Jeremy Jacob
Boolean Coherence: Does it make sense?
10:30‑11:30
Gerwin Klein (University of New South Wales)
Large-scale proof and libraries in Isabelle
11:30‑12:30
Andrzej Trybulec (University of Bialystok)
Mizar Mathematical Library - a large repository of formalized mathematics
10:30‑11:00
Vijay D'Silva, Leopold Haller and Daniel Kroening
SMT-Style Program Analysis with Value-based Refinements
11:00‑11:30
Stef Graillat, Fabienne Jézéquel and Yuxiang Zhu
Stochastic Arithmetic in Multiprecision
11:30‑12:00
Hong Diep Nguyen and Nathalie Revol
Doubling the precision for the residual and the solution in interval iterative refinement for linear system solving and certifying
12:00‑12:30
Vijay D'silva
Properties Provable with Abstract Domains.
10:30‑11:00
Andreas Abel
Integrating Sized and Dependent Types
11:00‑11:30
Thorsten Altenkirch and Nils Anders Danielsson
Termination Checking Nested Inductive and Coinductive Types
11:30‑12:00
Nils Anders Danielsson
Beating the Productivity Checker Using Embedded Languages
12:00‑12:30
Tarmo Uustalu
Antifounded coinduction in type theory
10:30‑11:10
Harley D. Eades III and Aaron Stump
Hereditary Substitution for Stratified System F
11:10‑11:50
Alexandre Viel and Dale Miller
Proof search when equality is a logical connective: Extended Abstract
11:50‑12:30
Arnaud Spiwack
An abstract type for constructing tactics in Coq
10:30‑11:00
M. Ganai, F. Ivancic
Efficient Decision Procedure for Non-linear Arithmetic Constraints using CORDIC
11:00‑11:30
E. Abraham, U. Loup, F. Corzilius, T. Sturm
A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra
11:30‑12:00
Frederic Besson
On using an inexact floating-point LP solver for deciding linear arithmetic in a SMT solver
12:00‑12:30
P. Rümmer and T. Wahl
An SMT-LIB Theory of Binary Floating-Point Arithmetic
10:30‑11:00
Makarius Wenzel
Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit
11:00‑11:30
Holger Gast
Engineering the Prover Interface
11:30‑12:00
Carst Tankink, Herman Geuvers and James McKinna
Narrating Formal Proof (Work in Progress)
12:00‑12:30
Freek Wiedijk
Pollack-inconsistency
10:30‑11:00
Hans Zantema
Length preserving string rewriting with exponential derivation length
11:00‑11:30
Martin Avanzini and Naohi Eguchi
A New Path Order for Exponential Time
11:30‑12:00
Harald Zankl and Martin Korp
The Derivational Complexity of the Bits Function and the Derivation Gap Principle
12:00‑12:30
Georg Moser and Andreas Schnabl
Dependency Graphs, Relative Rule Removal, the Subterm Criterion and Derivational Complexity
12:30‑14:00
Lunch
14:00‑15:00
Thomas Reps
There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code
14:00‑15:00
Michael Codish (Ben-Gurion University of the Negev, Israel)
Programming with Boolean Satisfaction
14:00‑14:30
Aiswarya Cyriac
A New Version of Focus Games for LTL Satisfiability
14:30‑15:00
Lukasz Kaiser and Tobias Ganzow
New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures
14:00‑15:00
Michael Clarkson (Cornell University)
Privacy in Electronic Voting
14:00‑15:00
Cindy Eisner (IBM Research Lab, Israel)
Invited talk: Why Work on Hardware Verification?
14:00‑15:00
David Pym (University of Aberdeen)
Modal Location-Resource-Process Logic for Access Control
14:00‑14:20
Tomi Janhunen
Modular Construction of Ground Logic Programs using LPCAT
14:20‑14:40
Amir Aavani, Xiongnan (Newman) Wu, Eugenia Ternovska and David Mitchell
Grounding Formulas with Complex Terms
14:40‑15:00
Johan Wittocx and Marc Denecker
Grounding FO(ID) with Bounds
14:00‑15:00
César A. Muñoz (NASA Langley)
A Mathematical Framework for the Verification of Air Traffic Separation Assurance Systems
14:00‑15:00
Don Sannella (University of Edinburgh)
Proofs in structured specifications
13:30‑14:30
Eric Feron (Dutton-Ducoffe Professor of Aerospace Engineering, Georgia Institute of Technology)
Applications of control to formal software semantics
14:30‑15:00
Stephen F. Siegel, Timothy Zirkel and Yi Wei
A Functional Equivalence Verification Suite for High-Performance Scientific Computing
14:00‑15:00
Conor McBride
Djinn, monotonic
14:00‑14:40
Zachary Snow, David Baelde and Gopalan Nadathur
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search
14:00‑14:30
D. Jovanovic and C. Barrett
Sharing is Caring
14:30‑15:00
L. Cordeiro, B Fischer
Bounded Model Checking of Multi-threaded Software using SMT solvers
14:00‑14:30
Tuan Minh Pham and Yves Bertot
A combination of a dynamic geometry software with a proof assistant for interactive formal proofs
14:30‑15:00
Vladimir Komendantsky, Alexander Konovalov and Steve Linton
Interfacing Coq + SSReflect with GAP
14:00‑14:30
Bernhard Gramlich and Felix Schernhammer
Outermost Termination via Contextual Dependency Pairs
14:30‑15:00
Cynthia Kop and Femke van Raamsdonk
Higher Order Dependency Pairs with Argument Filterings
15:00‑15:30
Coffee break
15:30‑16:00
Tutorial 3 continued
16:00‑17:30
Andrey Rybalchenko
Constraint Solving for Program Verification: Theory and Practice by Example
15:30‑16:00
Jan Wielemaker and Vítor Santos Costa
Portability of Prolog programs: theory and case-studies
16:00‑16:30
Dimitar Shterionov, Angelika Kimmig, Theofrastos Mantadelis and Gerda Janssens
DNF Sampling for ProbLog Inference
16:30‑17:00
Vasco Pedro and Salvador Abreu
Distributed Work Stealing for Constraint Solving
17:00‑17:30
Paulo André and Salvador Abreu
Casting the WAM as an EAM
17:30‑18:00
Gopal Gupta, Neda Saeedloei (University of Texas at Dallas)
Logic Programming Foundations of Cyber-Physical Systems
15:30‑16:30
Yevgeny Kazhakov (Oxford University, UK)
Consequence-Based Reasoning for Description Logic Ontologies
16:30‑17:30
Discussion
15:30‑16:00
Morten Dahl, Stéphanie Delaune and Graham Steel
Formal Analysis of Privacy for Vehicular Mix-Zones
16:00‑16:30
Tom Chothia, Konstantinos Chatzikokolakis and Apratim Guha
Calculating Information Leakage from System Tests: Mix Nodes and e-Passports
15:30‑16:00
Stefan Kupferschmid, Matthew Lewis, Bernd Becker and Tobias Schubert
Incremental Preprocessing Methods for use in BMC
16:00‑16:30
Souheib Baarir, Cecile Braunstein, Emmanuelle Encrenaz, Jean-Michel ILIE, Tun Li, Isabelle Mounier, Denis Poitrenaud and Sana Younes
Quantifying Robustness by Symbolic Model checking
16:30‑17:00
Gianpiero Cabodi, Sergio Nocco and Stefano Quer
Benchmarking a Model Checker for algorithmic improvements and tuning for performance
17:00‑17:30
Armin Biere
Discussion and Presentation of the Results of the 3rd Hardware Model Checking Competition
15:30‑16:00
Michael Köhler-Bußmeier
A Survey of Decidability Results for Elementary Object Systems
16:00‑16:30
Michael Köhler-Bußmeier and Frank Heitmann
Complexity of LTL Model-Checking for Safe Object Nets
16:30‑17:00
Michael Mendler and Stephan Scheele
Towards a Simply Typed CALculus for Semantic Knowledge Bases
15:30‑15:50
Emina Torlak.
Kodkod: A Constraint Solver for Relational Logic
15:50‑16:10
Gelsomina Catalano, Nicola Leone, and Simona Perri
The Intelligent Grounder of DLV
16:10‑16:30
Martin Gebser, Roland Kaminski and Torsten Schaub.
The Life of Gringo
16:30‑17:00
Discussion and Questions
15:30‑16:00
Yun Zhu, Edwin Westbrook, Jun Inoue, Alexandre Chapoutot, Cherif Salama, Marisa Peralta, Travis Martin, walid taha, Marcia O'Malley, Robert Cartwright, Aaron Ames and Raktim Bhattacharya
Mathematical Equations as Executable Models of Mechanical Systems
16:00‑16:30
Stefan Ratschan
Interval Constraint Propagation as a Tool for Deductions about Mixed Discrete/Continuous Systems
16:30‑16:45
Grant Olney Passmore and Paul B. Jackson
Introductory Tutorial: Combined Decision Techniques for the Existential Theory of the Reals
16:45‑17:15
Florent Kirchner and Grant Olney Passmore
Thinking Outside the (Arithmetic) Box: Certifying RAHD Computations
15:30‑16:30
Dale Miller (INRIA)
Towards a broad spectrum proof certificate
16:30‑17:30
Adam Chlipala (Harvard University)
A Bottom-Up Approach to Safe Low-Level Programming
15:30‑16:00
Stephen F. Siegel, Yi Wei and Timothy Zirkel
The Toolkit for Accurate Scientific Software
16:00‑17:30
Tool competition
15:30‑16:00
Claudio Sacerdoti Coen and Silvio Valentini
General recursion and formal topology
16:00‑16:30
Aaron Stump, Vilhelm Sjöberg and Stephanie Weirich
Termination Casts: A Flexible Approach to Termination with General Recursion
16:30‑17:00
Issam Maamria and Michael Butler
Rewriting and Well-Definedness within a Proof System
17:00‑17:30
Gavin Mendel-Gleason and Geoff Hamilton
Cyclic Proofs and Coinductive Principles
15:30‑16:30
David Baelde
An overview of focusing for least and greatest fixed points in intuitionistic logic
16:30‑17:30
Sean McLaughlin (Carnegie Mellon University)
The Inverse Method for Intuitionistic Modal Logic
15:30‑16:00
A. Griggio
A Practical Approach to SMT(LA(Z))
16:00‑16:30
A. Reynolds, L. Hadarean, C. Tinelli, Y. Ge, A. Stump, C. Barrett
Comparing Proof Systems for Linear Real Arithmetic with LFSC
16:30‑17:00
A report on the SMT Competition
15:30‑16:00
Andrei Lapets and Assaf Kfoury
A User-friendly Interface for a Lightweight Verification System
16:00‑16:30
Laura Meikle and Jacques Fleuriot
Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover's Palette
16:30‑18:00
UITP Steering/Programme Committee
Business Meeting and After Hours Demos
15:30‑16:00
Jean-Pierre Jouannaud and Jian-qi Li
A Computability Path Ordering for Polymorphic Terms
16:00‑16:30
Nachum Dershowitz
An Abstract Path Ordering
16:30‑17:00
Business Meeting