VSL 2014: VIENNA SUMMER OF LOGIC 2014

CAV ON TUESDAY, JULY 22ND: TALK VIEW

Days:
previous day
all days

View: with abstractssession overviewside by side with other conferences

9:00
9:30
10:00
10:30
11:00
11:30
12:00
12:30
13:00
13:30
14:00
14:30
15:00
15:30
16:00
16:30
17:00
17:30
18:00
18:30
10:45-11:05
Monadic Decomposition
Margus Veanes, Nikolaj Bjorner, Lev Nachmanson, Sergey Bereg
11:05-11:25
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters
11:25-11:45
Bit-Vector Rewriting with Automatic Rule Generation
Alexander Nadel
11:45-12:05
A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors
Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, Kshitij Bansal
12:05-12:25
AVATAR: The New Architecture for First-Order Theorem Provers
Andrei Voronkov
12:25-12:45
Automating Separation Logic with Trees and Data
Ruzica Piskac, Thomas Wies, Damien Zufferey
12:45-12:55
A Nonlinear Real Arithmetic Fragment
Ashish Tiwari, Patrick Lincoln
12:55-13:05
Yices 2.2
Bruno Dutertre
10:45-11:05
Monadic Decomposition
Margus Veanes, Nikolaj Bjorner, Lev Nachmanson, Sergey Bereg
11:05-11:25
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters
11:25-11:45
Bit-Vector Rewriting with Automatic Rule Generation
Alexander Nadel
11:45-12:05
A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors
Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, Kshitij Bansal
12:05-12:25
AVATAR: The New Architecture for First-Order Theorem Provers
Andrei Voronkov
12:25-12:45
Automating Separation Logic with Trees and Data
Ruzica Piskac, Thomas Wies, Damien Zufferey
12:45-12:55
A Nonlinear Real Arithmetic Fragment
Ashish Tiwari, Patrick Lincoln
12:55-13:05
Yices 2.2
Bruno Dutertre
14:30-14:50
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
Moritz Sinn, Florian Zuleger, Helmut Veith
14:50-15:10
Symbolic Resource Bound Inference for Functional Programs
Ravichandhran Madhavan, Viktor Kuncak
15:10-15:30
Proving Non-termination Using Max-SMT
D. Larraz, K. Nimkar, A. Oliveras, E. Rodríguez-Carbonell, A. Rubio
15:30-15:50
Termination Analysis by Learning Terminating Programs
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
15:50-16:10
Causal Termination of Multi-threaded Programs
Andrey Kupriyanov, Bernd Finkbeiner
16:40-17:00
Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher
17:00-17:20
Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath
Suho Lee, Karem A. Sakallah
17:20-17:30
QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan
17:30-18:30 Business Meeting
08:45-09:45
VSL Keynote Talk: Verification of Computer Systems with Model Checking
Edmund Clarke
10:15-10:45 Coffee Break
13:00-14:30 Lunch Break
16:00-16:30 Coffee Break
Disclaimer | Powered by EasyChair Smart Program