CAV Program

10:45	Jean-Christophe Filliatre, Léon Gondelman and Andrei Paskevich The Spirit of Ghost Code (abstract)
11:05	Anvesh Komuravelli, Arie Gurfinkel and Sagar Chaki SMT-based Model Checking for Recursive Programs (abstract)
11:25	Shachar Itzhaky, Nikolaj Bjørner, Thomas Reps, Mooly Sagiv and Aditya Thakur Property-Directed Shape Analysis (abstract)
11:45	Quang Loc Le, Cristian Gherghina, Shengchao Qin and Wei-Ngan Chin Shape Analysis via Second-Order Bi-Abduction (abstract)
12:05	Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider ICE: A Robust Learning Framework for Synthesizing Invariants (abstract)
12:25	Rahul Sharma and Alex Aiken From Invariant Checking to Invariant Inference Using Randomized Search (abstract)
12:45	Zvonimir Rakamaric and Michael Emmi SMACK: Decoupling Source Language Details from Verifier Implementations (abstract)
12:55	Rajeev Alur 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	Christos Dimoulas, Scott Moore, Aslan Askarov and Stephen Chong Declarative Policies for Capability Control (abstract)
11:15	Joshua Kroll, Gordon Stewart and Andrew Appel Portable Software Fault Isolation (abstract)
11:45	Radha Jagadeesan, Cm Lubinski, Corin Pitcher, James Riely and Charles Winebrinner Certificates for Verifiable Forensics (abstract)
12:15	Andrey Chudnov, George Kuan and David Naumann 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:

Somesh Jha

Location: FH, Hörsaal 1

14:30	Hassan Eldib and Chao Wang Synthesis of Masking Countermeasures against Side Channel Attacks (abstract)
14:50	Omar Chowdhury, Limin Jia, Deepak Garg and Anupam Datta Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (abstract)
15:10	Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp Reummer and Jari Stenman Program Verification through String Rewriting (abstract)
15:30	Sudeep Kanav, Peter Lammich and Andrei Popescu A Conference Management System with Verified Document Confidentiality (abstract)
15:50	Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen and Gennaro Parlato 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)

Chair:

Roberto Sebastiani

Location: FH, Hörsaal 5

14:30	Ori Lahav and Yoni Zohar SAT-based Decision Procedure for Analytic Pure Sequent Calculi (abstract)
15:00	Marijn Heule, Martina Seidl and Armin Biere A Unified Proof System for QBF Preprocessing (abstract)
15:30	Carlos Ansótegui, Maria Luisa Bonet, Jesus Giráldez-Cru and Jordi Levy The Fractal Dimension of SAT Formulas (abstract)

16:00-16:30Coffee Break

16:30-17:10 Session 116A: Automata

Chair:

Bernd Finkbeiner

Location: FH, Hörsaal 1

16:30	Javier Esparza and Jan Kretinsky From LTL to Deterministic Automata: A Safraless Compositional Approach (abstract)
16:50	Loris D'Antoni and Rajeev Alur Symbolic Visibly Pushdown Automata (abstract)

16:30-17:00 Session 116C: FLoC Inter-Conference Topic: SAT/SMT/QBF (joint with IJCAR)

Chair:

Uwe Waldmann

Location: FH, Hörsaal 5

16:30

Paula Chocron, Pascal Fontaine and Christophe Ringeissen

A Gentle Non-Disjoint Combination of Satisfiability Procedures (abstract)

17:10-18:00 Session 119A: Invited Talk

Chair:

Armin Biere

Location: FH, Hörsaal 1

17:10

Erik Winfree

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	Pablo Buiras, Deian Stefan and Alejandro Russo On Dynamic Flow-sensitive Floating-Label Systems (abstract)
18:00	Heiko Mantel, Matthias Perner and Jens Sauer Noninterference under Weak Memory Models (abstract)

18:00-18:30 Session 121: CAV Award Ceremony

Chair:

Marta Kwiatkowska

Location: FH, Hörsaal 1

19:00-21:30 Session 122: VSL Reception 2

Location: University of Vienna, Arkadenhof

Sunday, July 20th, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

08:45-10:15 Session 123: FLoC Plenary Talk (joint with 9 other meetings)

Chair:

Andrei Voronkov

Location: FH, Hörsaal 1

08:45

Véronique Cortier

FLoC Plenary Talk: Electronic voting: how logic can help? (abstract)

Saturday, July 19th, 2014

View this program: with abstracts session overview talk overview side 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 abstracts session overview talk overview side by side with other conferences

10:15-10:45Coffee Break

10:15-18:00 Session 126A: FLoC Olympic Games Big Screen: CASC Automated Theorem Proving System Competition (CASC-J7) (joint with 9 other meetings)

Location: FH, 2nd floor

10:15

Geoff Sutcliffe

FLoC Olympic Games Big Screen: 7th IJCAR ATP System Competition (CASC-J7) (abstract)

10:15-18:00 Session 126B: FLoC Olympic Games Big Screen: Termination Competition (termComp) (joint with 9 other meetings)

Location: FH, 2nd floor

10:15

Jürgen Giesl, Stefan von der Krone, Frederic Mesnard, Albert Rubio, René Thiemann and Johannes Waldmann

FLoC Olympic Games Big Screen: Termination Competition (termCOMP 2014) (abstract)

10:45-13:05 Session 127C: Model Checking and Testing

Chair:

Natasha Sharygina

Location: FH, Hörsaal 1

10:45	Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair Donaldson, Jeroen Ketema, Dan Liew and Shaz Qadeer Engineering a Static Verification Tool for GPU Kernels (abstract)
11:05	Kenneth McMillan Lazy Annotation Revisited (abstract)
11:25	Yakir Vizel and Arie Gurfinkel Interpolating Property Directed Reachability (abstract)
11:45	Jesse Bingham and Joe Leslie-Hurd Verifying Relative Error Bounds using Symbolic Simulation (abstract)
12:05	Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi and Darko Marinov Regression Test Selection for Distributed Software Histories (abstract)
12:25	Anton Wijs, Joost-Pieter Katoen and Dragan Bosnacki GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (abstract)
12:45	Dirk Beyer, Georg Dresler and Philipp Wendler Software Verification in the Google App-Engine Cloud (abstract)
12:55	Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri and Stefano Tonetta The nuXmv Symbolic Model Checker (abstract)

13:00-14:30Lunch Break

14:30-16:00 Session 129C: Biology and Hybrid Systems

Chair:

Marta Kwiatkowska

Location: FH, Hörsaal 1

14:30	Armin Biere Hardware Model Checking Competition 2014 CAV Edition (abstract)
14:40	Hillel Kugler, Nicola Paoletti, Boyan Yordanov, Youssef Hamadi and Christoph M. Wintersteiger Analyzing and Synthesizing Genomic Logic Functions (abstract)
15:00	Byron Cook, Jasmin Fisher, Benjamin Hall, Samin Ishtiaq, Garvit Juniwal and Nir Piterman Finding instability in biological models (abstract)
15:20	Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra and Marta Kwiatkowska Invariant verification of nonlinear hybrid automata networks of cardiac cells (abstract)
15:40	Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen and Jun Sun Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (abstract)

14:30-16:00 Session 129G: FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (joint with 9 other meetings)

Location: FH, Hörsaal 2

14:30

Francesco Calimeri, Martin Gebser, Marco Maratea and Francesco Ricca

FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (abstract)

16:00-16:30Coffee Break

16:30-17:10 Session 130C: Hybrid Systems

Chair:

Rajeev Alur

Location: FH, Hörsaal 1

16:30	Willem Hagemann Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections (abstract)
16:50	Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta Verifying LTL properties of hybrid systems with K-liveness (abstract)

17:10-18:00 Session 131: Invited Talk

Chair:

Roderick Bloem

Location: FH, Hörsaal 1

17:10

Rance Cleaveland

Automated Testing (preliminary title) (abstract)

Monday, July 21st, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

10:45-13:05 Session 138C: Games and Synthesis

Chair:

Barbara Jobstmann

Location: FH, Hörsaal 1

10:45	Rodica Bozianu, Catalin Dima and Emmanuel Filiot Safraless Synthesis for Epistemic Temporal Specifications (abstract)
11:05	Tomas Brazdil, David Klaska, Antonin Kucera and Petr Novotný Minimizing Running Costs in Consumption Systems (abstract)
11:25	Krishnendu Chatterjee, Martin Chmelík and Przemyslaw Daca CEGAR for Qualitative Analysis of Probabilistic Systems (abstract)
11:45	Thomas Dillig, Isil Dillig and Swarat Chaudhuri Optimal Guard Synthesis for Memory Safety (abstract)
12:05	Jade Alglave, Daniel Kroening, Vincent Nimal and Daniel Poetzl Don't sit on the fence: A static analysis approach to automatic fence insertion (abstract)
12:25	Petr Čermák, Alessio Lomuscio, Fabio Mogavero and Aniello Murano MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (abstract)
12:35	Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Walker Solving Games without Controllable Predecessor (abstract)
12:45	Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess and Stefan Stattelmann G4LTL-ST: Automatic Generation of PLC Programs (abstract)
12:55	Roderick Bloem, Ruediger Ehlers and Swen Jacobs SYNTCOMP - Synthesis Competition for Reactive Systems (abstract)

14:30-16:00 Session 140C: Concurrency

Chair:

Azadeh Farzan

Location: FH, Hörsaal 1

14:30	Mohsen Lesani, Todd Millstein and Jens Palsberg Automatic Atomicity Verification for Clients of Concurrent Data Structures (abstract)
14:50	Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach Regression-free Synthesis for Concurrency (abstract)
15:10	Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre and Gennaro Parlato Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (abstract)
15:30	Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp Meyer and Filip Niksic An SMT-Based Approach to Coverability Analysis (abstract)
15:50	Alejandro Sanchez and Cesar Sanchez 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)

Chair:

Pascal Fontaine

Location: FH, Hörsaal 5

14:30	Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Ruemmer Approximations for Model Construction (abstract)
15:00	Rüdiger Ehlers and Martin Lange A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (abstract)
15:20	Aaron Stump, Geoff Sutcliffe and Cesare Tinelli StarExec: a Cross-Community Infrastructure for Logic Solving (abstract)
15:40	Bruno Woltzenlogel Paleo, Joseph Boudou and Andreas Fellner Skeptik [System Description] (abstract)

Sunday, July 20th, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

19:00-21:30 Session 142: VSL Banquet 2

Location: Schönbrunn

Monday, July 21st, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

08:45-10:15 Session 144A: VSL Keynote Talk

Chair:

Thomas Eiter

Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1

08:45

Franz Baader

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

Friedrich Stadler

VSL Public Lecture: Vienna Circle(s) - Between Philosophy and Science in Cultural Context (abstract)

Tuesday, July 22nd, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

10:45-13:05 Session 149C: FLoC Inter-Conference Topic: SAT/SMT/QBF (joint with IJCAR)

Chair:

Orna Grumberg

Location: FH, Hörsaal 1

10:45	Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg Monadic Decomposition (abstract)
11:05	Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Morgan Deters A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (abstract)
11:25	Alexander Nadel Bit-Vector Rewriting with Automatic Rule Generation (abstract)
11:45	Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli and Kshitij Bansal A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (abstract)
12:05	Andrei Voronkov AVATAR: The New Architecture for First-Order Theorem Provers (abstract)
12:25	Ruzica Piskac, Thomas Wies and Damien Zufferey Automating Separation Logic with Trees and Data (abstract)
12:45	Ashish Tiwari and Patrick Lincoln A Nonlinear Real Arithmetic Fragment (abstract)
12:55	Bruno Dutertre Yices 2.2 (abstract)

Monday, July 21st, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

16:30-19:00 Session 151A: VSL Joint Award Ceremony 2

Chair:

Helmut Veith

Location: MB, Kuppelsaal

16:30	Floc Olympic Games FLoC Olympic Games Award Ceremony 2 (abstract)
18:00	Werner Depauli-Schimanovich Lifetime Achievement Award (abstract)
18:10	Mingyi Zhang Lifetime Achievement Award (abstract)
18:20	European Masters Program In Computational Logic EMCL Distinguished Alumni Award (abstract)
18:30	Helmut Veith FLoC Closing Week 2 (abstract)

Tuesday, July 22nd, 2014

View this program: with abstracts session overview talk overview side by side with other conferences

14:30-16:10 Session 151C: Bounds and Termination

Chair:

Pavol Cerny

Location: FH, Hörsaal 1

14:30	Moritz Sinn, Florian Zuleger and Helmut Veith A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (abstract)
14:50	Ravichandhran Madhavan and Viktor Kuncak Symbolic Resource Bound Inference for Functional Programs (abstract)
15:10	Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio Proving Non-termination Using Max-SMT (abstract)
15:30	Matthias Heizmann, Jochen Hoenicke and Andreas Podelski Termination Analysis by Learning Terminating Programs (abstract)
15:50	Andrey Kupriyanov and Bernd Finkbeiner Causal Termination of Multi-threaded Programs (abstract)

16:40-17:30 Session 154: Abstraction

Chair:

Doron Peled

Location: FH, Hörsaal 1

16:40	Johannes Birgmeier, Aaron R. Bradley and Georg Weissenbacher Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (abstract)
17:00	Suho Lee and Karem A. Sakallah Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (abstract)
17:20	Arlen Cox, Bor-Yuh Evan Chang and Sriram Sankaranarayanan QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (abstract)

17:30-18:30 Session 156: Business Meeting

Location: FH, Hörsaal 1

08:45-10:15 Session 156: VSL Keynote Talk

Chair:

Helmut Veith

Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1

08:45

Edmund Clarke

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