Days: Friday, July 18th Saturday, July 19th Sunday, July 20th Monday, July 21st Tuesday, July 22nd
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:45 | FLoC Plenary Talk: From Reachability to Temporal Specifications in Game Theory (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:45 | FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change? (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:45 | How do we get inductive invariants? (Part A) (abstract) |
09:00 | FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (abstract) |
09:00 | FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (abstract) |
10:45 | How do we get inductive invariants? (Part B) (abstract) |
14:30 | Hardware Model Checking (Part A) (abstract) |
16:30 | Hardware Model Checking (Part B) (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:45 | FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (abstract) |
10:45 | The Spirit of Ghost Code (abstract) |
11:05 | SMT-based Model Checking for Recursive Programs (abstract) |
11:25 | Property-Directed Shape Analysis (abstract) |
11:45 | Shape Analysis via Second-Order Bi-Abduction (abstract) |
12:05 | ICE: A Robust Learning Framework for Synthesizing Invariants (abstract) |
12:25 | From Invariant Checking to Invariant Inference Using Randomized Search (abstract) |
12:45 | SMACK: Decoupling Source Language Details from Verifier Implementations (abstract) |
12:55 | Syntax-Guided Synthesis Competition Results (abstract) |
10:45 | Declarative Policies for Capability Control (abstract) |
11:15 | Portable Software Fault Isolation (abstract) |
11:45 | Certificates for Verifiable Forensics (abstract) |
12:15 | Information flow monitoring as abstract interpretation for relational logic (abstract) |
14:30 | Synthesis of Masking Countermeasures against Side Channel Attacks (abstract) |
14:50 | Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (abstract) |
15:10 | Program Verification through String Rewriting (abstract) |
15:30 | A Conference Management System with Verified Document Confidentiality (abstract) |
15:50 | VAC - Verifier of Administrative Role-based Access Control Policies (abstract) |
14:30 | SAT-based Decision Procedure for Analytic Pure Sequent Calculi (abstract) |
15:00 | A Unified Proof System for QBF Preprocessing (abstract) |
15:30 | The Fractal Dimension of SAT Formulas (abstract) |
16:30 | From LTL to Deterministic Automata: A Safraless Compositional Approach (abstract) |
16:50 | Symbolic Visibly Pushdown Automata (abstract) |
16:30 | A Gentle Non-Disjoint Combination of Satisfiability Procedures (abstract) |
17:10 | Designing and verifying molecular circuits and systems made of DNA (abstract) |
17:30 | On Dynamic Flow-sensitive Floating-Label Systems (abstract) |
18:00 | Noninterference under Weak Memory Models (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:45 | FLoC Plenary Talk: Electronic voting: how logic can help? (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
View this program: with abstractssession overviewtalk overviewside by side with other conferences
10:15 | FLoC Olympic Games Big Screen: 7th IJCAR ATP System Competition (CASC-J7) (abstract) |
10:15 | FLoC Olympic Games Big Screen: Termination Competition (termCOMP 2014) (abstract) |
10:45 | Engineering a Static Verification Tool for GPU Kernels (abstract) |
11:05 | Lazy Annotation Revisited (abstract) |
11:25 | Interpolating Property Directed Reachability (abstract) |
11:45 | Verifying Relative Error Bounds using Symbolic Simulation (abstract) |
12:05 | Regression Test Selection for Distributed Software Histories (abstract) |
12:25 | GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (abstract) |
12:45 | Software Verification in the Google App-Engine Cloud (abstract) |
12:55 | The nuXmv Symbolic Model Checker (abstract) |
14:30 | Hardware Model Checking Competition 2014 CAV Edition (abstract) |
14:40 | Analyzing and Synthesizing Genomic Logic Functions (abstract) |
15:00 | Finding instability in biological models (abstract) |
15:20 | Invariant verification of nonlinear hybrid automata networks of cardiac cells (abstract) |
15:40 | Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (abstract) |
14:30 | FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (abstract) |
16:30 | Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (abstract) |
16:50 | Verifying LTL properties of hybrid systems with K-liveness (abstract) |
17:10 | Automated Testing (preliminary title) (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
10:45 | Safraless Synthesis for Epistemic Temporal Specifications (abstract) |
11:05 | Minimizing Running Costs in Consumption Systems (abstract) |
11:25 | CEGAR for Qualitative Analysis of Probabilistic Systems (abstract) |
11:45 | Optimal Guard Synthesis for Memory Safety (abstract) |
12:05 | Don't sit on the fence: A static analysis approach to automatic fence insertion (abstract) |
12:25 | MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (abstract) |
12:35 | Solving Games without Controllable Predecessor (abstract) |
12:45 | G4LTL-ST: Automatic Generation of PLC Programs (abstract) |
12:55 | SYNTCOMP - Synthesis Competition for Reactive Systems (abstract) |
14:30 | Automatic Atomicity Verification for Clients of Concurrent Data Structures (abstract) |
14:50 | Regression-free Synthesis for Concurrency (abstract) |
15:10 | Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (abstract) |
15:30 | An SMT-Based Approach to Coverability Analysis (abstract) |
15:50 | LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (abstract) |
14:30 | Approximations for Model Construction (abstract) |
15:00 | A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (abstract) |
15:20 | StarExec: a Cross-Community Infrastructure for Logic Solving (abstract) |
15:40 | Skeptik [System Description] (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:45 | VSL Keynote Talk: Ontology-Based Monitoring of Dynamic Systems (abstract) |
19:00 | VSL Public Lecture: Vienna Circle(s) - Between Philosophy and Science in Cultural Context (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
10:45 | Monadic Decomposition (abstract) |
11:05 | A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (abstract) |
11:25 | Bit-Vector Rewriting with Automatic Rule Generation (abstract) |
11:45 | A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (abstract) |
12:05 | AVATAR: The New Architecture for First-Order Theorem Provers (abstract) |
12:25 | Automating Separation Logic with Trees and Data (abstract) |
12:45 | A Nonlinear Real Arithmetic Fragment (abstract) |
12:55 | Yices 2.2 (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
16:30 | FLoC Olympic Games Award Ceremony 2 (abstract) |
18:00 | Lifetime Achievement Award (abstract) |
18:10 | Lifetime Achievement Award (abstract) |
18:20 | EMCL Distinguished Alumni Award (abstract) |
18:30 | FLoC Closing Week 2 (abstract) |
View this program: with abstractssession overviewtalk overviewside by side with other conferences
14:30 | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (abstract) |
14:50 | Symbolic Resource Bound Inference for Functional Programs (abstract) |
15:10 | Proving Non-termination Using Max-SMT (abstract) |
15:30 | Termination Analysis by Learning Terminating Programs (abstract) |
15:50 | Causal Termination of Multi-threaded Programs (abstract) |
16:40 | Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (abstract) |
17:00 | Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (abstract) |
17:20 | QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (abstract) |
08:45 | VSL Keynote Talk: Verification of Computer Systems with Model Checking (abstract) |