HTTP/1.1 200 OK Date: Fri, 16 Jan 2026 11:24:10 GMT Server: Apache/2.4.41 (Ubuntu) Expires: Fri, 16 Jan 2026 11:24:10 GMT Connection: close Vary: Accept-Encoding Content-Encoding: gzip Content-Length: 12614 Content-Type: text/html; charset=UTF-8

VSL 2014: VIENNA SUMMER OF LOGIC 2014 VSLPROGRAMINDEXES VSL | FLoC | CAV | CSF | CSL-LICS | ICLP | IJCAR | ITP | RTA-TLCA | SAT | LC | LATD | KR | DL | NMR | 2FC | ACL2 | ADDCT | AISS | APPA | ARQNL | ARW-DT | ASA | ASPOCP | Automatheo | CHR | CICLOPS-WLPE | CLC | Coq | CSPSAT | DCM | DTP | EC2 | FCS-FCC | FRIDA | FWFM | GeTFun | GSB | HCVS | HOL | HOPA | HOR | HSB | IFIP-WG16 | INFINITY | iPRA | ITRS | IWC | Isabelle | KInAR | KR4HC | LaSh | LCC | LFMTP | LG | Linearity | LOLA | LSB | NCPROOFS | NLCS | NLSR | NSV | ORE | PAAR | ParSearchOpt | PAS | PC | PCCR | PLP | POS | PRUV | PSC | QBF | QED | QUANTIFY | RCRA | REORDER | RS | SMT | SD | SSV | STAST | SYNT | TermGraph | UITP | UNIF | Vampire | VEMDP | VERIFY | VeriSure | VPT | VSTTE | WING | WIR | WPTE | WST | WWV PC | HOME | CFP | PROGRAM | INDEXES 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) Chair: Moshe Vardi Location: FH, Hörsaal 1 08:45 Orna Kupfermann 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) Chair: Moshe Vardi Location: FH, Hörsaal 1 08:45 Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel and Andrei Voronkov 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? Chair: Armin Biere Location: FH, Hörsaal 6 08:45 David Monniaux How do we get inductive invariants? (Part A) (abstract) 09:00-18:00 Session 87D: FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (joint with 9 other meetings) Location: EI, Foyer 09:00 Birte Glimm, Nicolas Matentzoglu, Bijan Parsia and Andreas Steigmiller FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (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 David Cok, David Deharbe and Tjark Weber 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? Chair: Armin Biere Location: FH, Hörsaal 6 10:45 David Monniaux How do we get inductive invariants? (Part B) (abstract) 13:00-14:30Lunch Break 14:30-16:00 Session 96AD: Tutorial: Hardware Model Checking Chair: Roderick Bloem Location: FH, Hörsaal 6 14:30 Fabio Somenzi Hardware Model Checking (Part A) (abstract) 16:00-16:30Coffee Break 16:30-18:00 Session 99AB: Tutorial: Hardware Model Checking Chair: Roderick Bloem Location: FH, Hörsaal 6 16:30 Fabio Somenzi 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) Chair: Helmut Veith Location: FH, Hörsaal 1 08:45 Fahiem Bacchus, Armin Biere, Byron Cook, Joel Ouaknine, Karem Sakallah and Mirek Truszczynski FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (abstract) 10:15-10:45Coffee Break 10:45-13:05 Session 109A: Software Verification Chair: Domagoj Babic Location: FH, Hörsaal 1 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 abstractssession overviewtalk overviewside 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 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: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 abstractssession overviewtalk overviewside 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 abstractssession overviewtalk overviewside 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 abstractssession overviewtalk overviewside 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 abstractssession overviewtalk overviewside 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 abstractssession overviewtalk overviewside 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 abstractssession overviewtalk overviewside 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 Disclaimer | Powered by EasyChair Smart Program