VSL 2014: VIENNA SUMMER OF LOGIC 2014
CAV PROGRAM

Days: Friday, July 18th Saturday, July 19th Sunday, July 20th Monday, July 21st Tuesday, July 22nd

Tuesday, July 15th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:45-10:15 Session 44: FLoC Plenary Talk (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Plenary Talk: From Reachability to Temporal Specifications in Game Theory (abstract)
Thursday, July 17th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:45-10:15 Session 62A: FLoC Panel (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change? (abstract)
Friday, July 18th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:45-10:15 Session 86B: Tutorial: How do we get inductive invariants?
Location: FH, Hörsaal 6
08:45
How do we get inductive invariants? (Part A) (abstract)
09:00-18:00 Session 87E: FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (joint with 9 other meetings)
Location: FH, 2nd floor
09:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (abstract)
10:15-10:45Coffee Break
10:45-12:15 Session 90AD: Tutorial: How do we get inductive invariants?
Location: FH, Hörsaal 6
10:45
How do we get inductive invariants? (Part B) (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 96AD: Tutorial: Hardware Model Checking
Location: FH, Hörsaal 6
14:30
Hardware Model Checking (Part A) (abstract)
16:00-16:30Coffee Break
16:30-18:00 Session 99AB: Tutorial: Hardware Model Checking
Location: FH, Hörsaal 6
16:30
Hardware Model Checking (Part B) (abstract)
Saturday, July 19th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:45-10:15 Session 106A: FLoC Panel (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (abstract)
10:15-10:45Coffee Break
10:45-13:05 Session 109A: Software Verification
Location: FH, Hörsaal 1
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-12:45 Session 109D: FLoC Inter-Conference Topic: Security. Software Security (joint with CSF)
Location: FH, Hörsaal 6
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)
13:00-14:30Lunch Break
14:30-16:00 Session 113A: FLoC Inter-Conference Topic: Security (joint with CSF)
Chair:
Location: FH, Hörsaal 1
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-16:00 Session 113C: FLoC Inter-Conference Topic: SAT/SMT/QBF (joint with IJCAR)
Location: FH, Hörsaal 5
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:00-16:30Coffee Break
16:30-17:10 Session 116A: Automata
Location: FH, Hörsaal 1
16:30
From LTL to Deterministic Automata: A Safraless Compositional Approach (abstract)
16:50
Symbolic Visibly Pushdown Automata (abstract)
16:30-17:00 Session 116C: FLoC Inter-Conference Topic: SAT/SMT/QBF (joint with IJCAR)
Location: FH, Hörsaal 5
16:30
A Gentle Non-Disjoint Combination of Satisfiability Procedures (abstract)
17:10-18:00 Session 119A: Invited Talk
Location: FH, Hörsaal 1
17:10
Designing and verifying molecular circuits and systems made of DNA (abstract)
17:30-18:30 Session 120: FLoC Inter-Conference Topic: Security. Information Flow 1 (joint with CSF)
Location: FH, Hörsaal 6
17:30
On Dynamic Flow-sensitive Floating-Label Systems (abstract)
18:00
Noninterference under Weak Memory Models (abstract)
19:00-21:30 Session 122: VSL Reception 2
Location: University of Vienna, Arkadenhof
Sunday, July 20th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:45-10:15 Session 123: FLoC Plenary Talk (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Plenary Talk: Electronic voting: how logic can help? (abstract)
Saturday, July 19th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

22:00-23:59 Session 123: VSL Student Reception 2
Location: Säulenhalle (Volksgarten)
Sunday, July 20th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

10:15-10:45Coffee Break
10:45-13:05 Session 127C: Model Checking and Testing
Location: FH, Hörsaal 1
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)
13:00-14:30Lunch Break
14:30-16:00 Session 129C: Biology and Hybrid Systems
Location: FH, Hörsaal 1
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)
16:00-16:30Coffee Break
16:30-17:10 Session 130C: Hybrid Systems
Location: FH, Hörsaal 1
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-18:00 Session 131: Invited Talk
Location: FH, Hörsaal 1
17:10
Automated Testing (preliminary title) (abstract)
Monday, July 21st, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

10:45-13:05 Session 138C: Games and Synthesis
Location: FH, Hörsaal 1
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-16:00 Session 140C: Concurrency
Location: FH, Hörsaal 1
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-16:00 Session 140E: FLoC Inter-Conference topic: SAT/SMT/QBF (joint with IJCAR)
Location: FH, Hörsaal 5
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)
Sunday, July 20th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

Monday, July 21st, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:45-10:15 Session 144A: VSL Keynote Talk
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
08:45
VSL Keynote Talk: Ontology-Based Monitoring of Dynamic Systems (abstract)
10:15-10:45Coffee Break
13:00-14:30Lunch Break
16:00-16:30Coffee Break
19:00-20:00 Session 149A: VSL Public Lecture 2
Location: MB, Kuppelsaal
19:00
VSL Public Lecture: Vienna Circle(s) - Between Philosophy and Science in Cultural Context (abstract)
Tuesday, July 22nd, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

10:45-13:05 Session 149C: FLoC Inter-Conference Topic: SAT/SMT/QBF (joint with IJCAR)
Location: FH, Hörsaal 1
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)
Monday, July 21st, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

16:30-19:00 Session 151A: VSL Joint Award Ceremony 2
Location: MB, Kuppelsaal
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)
Tuesday, July 22nd, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

14:30-16:10 Session 151C: Bounds and Termination
Location: FH, Hörsaal 1
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-17:30 Session 154: Abstraction
Location: FH, Hörsaal 1
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-10:15 Session 156: VSL Keynote Talk
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
08:45
VSL Keynote Talk: Verification of Computer Systems with Model Checking (abstract)
10:15-10:45Coffee Break
13:00-14:30Lunch Break
16:00-16:30Coffee Break