8:30 Welcome
8:35-9:35 Invited talk: Cynthia Dwork (Chair: Ken McMillan)
9:35-10:05 Session 1: SAT-based synthesis (Chair: Ken McMillan)
9:35 SAT-Based Synthesis Methods for Safety Specs:
Roderick Bloem, Robert Koenighofer and Martina Seidl.
10:05-10:30 Break
10:30-12:00 Session 2: Abstract interpretation of concurrent
programs (Chair: Jérôme Feret)
10:30 Precise analysis of value-dependent synchronization in programs
with priority scheduling:
Martin Schwarz, Helmut Seidl, Vesal Vojdani and Kalmer Apinis.
11:00 Relational Thread-Modular Static Value Analysis by Abstract
Interpretation:
Antoine Miné.
11:30 Timing Analysis of Parallel Software Using Abstract Execution:
Andreas Gustavsson, Jan Gustafsson and Björn Lisper.
12:00-13:30 Lunch
13:30-14:30 Invited talk: Prakash Panangaden (Chair: Xavier Rival)
14:30-15:00 Session 3: Omega-regular games (Chair: Xavier Rival)
14:30 Doomsday Equilibria for Omega-Regular Games:
Krishnendu Chatterjee, Laurent Doyen, Emmanuel Filiot and Jean-Francois Raskin.
15:00-15:30 Break
15:30-16:30 Session 4: Probabilistic techniques (Chair:
Prakash Panangaden)
15:30 Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes:
Lei Song, Lijun Zhang and Jens Chr. Godskesen.
16:00 Probabilistic Automata for Safety LTL Specifications:
Dileep Kini and Mahesh Viswanathan.
Monday, January 20
8:30-9:30 Invited talk: Bor-Yuh Evan Chang (Chair: Ken McMillan)
9:30-10:00 Session 5: Tools (Chair: Ken McMillan)
9:30 Cascade 2.0 (Tool Paper):
Wei Wang, Clark Barrett and Thomas Wies.
10:00-10:30 Break
10:30-12:00 Session 6: Verification and transformation
(Chair: David Schmidt)
10:30 A Logic-based Framework for Verifying Consensus Algorithms:
Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder and Damien Zufferey.
11:00 Verifying Array Programs by Transforming Verification Conditions:
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti.
11:30 Weakest Precondition Synthesis for Compiler Optimizations:
Nuno P. Lopes and Jose Monteiro.
12:00-13:30 Lunch
13:30-15:00 Session 7: Model checking and state space
reduction (Chair: Andreas Podelski)
13:30 Message Passing Algorithms for the Verification of Distributed Protocols:
Loig Jezequel and Javier Esparza.
14:00 Safety Problems are NP-complete for Flat Integer Programs with
Octagonal Loop:
Radu Iosif, Marius Bozga and Filip Konecny.
14:30 Parameterized Model Checking of Token-Passing Systems:
Benjamin Aminof, Swen Jacobs, Ayrat Khalimov and Sasha Rubin.
15:00-15:30 Break
15:30-16:30 Session 8: Combining heap and numeric analyses
(Chair: Bor-Yuh Evan Chang)
15:30 Modularly Combining Numeric Abstract Domains with Points-to Analysis,
and a Scalable Static Numeric Analyzer for Java:
Zhoulai Fu.
16:00 Generic Combination of Heap and Value Analyses in Abstract Interpretation:
Pietro Ferrara.
18:30 Social event at Candelas Restaurant, 416 3rd Ave, San Diego
18:30 Drinks.
19:30 Dinner.
Tuesday, January 21
8:30-9:30 Invited talk: Thomas Wies (chair: Xavier Rival)
9:30-10:00 Session 9: Applications to biology
(Chair: Jérôme Feret)
9:30 Modelling parsimonious putative regulatory networks: complexity and
heuristic approaches:
Vicente Acuña, Andres Aravena, Alejandro Maass and Anne Siegel.
10:00-10:30 Break
10:30-12:00 Session 10: Dynamic verification
(Chair: Rustan Leino)
10:30 Practical Floating-Point Tests with Integer Code:
Anthony Romano.
11:00 Monitoring Parametric Temporal Logic:
Peter Faymonville, Bernd Finkbeiner and Doron Peled.
11:30 Deciding Control State Reachability in Concurrent Traces with
Limited Observability:
Chao Wang and Kevin Hoang.
12:00-13:30 Lunch
13:30-15:00 Session 11: Synthesis
(Chair: Lenore Zuck)
13:30 Modular Synthesis of Sketches using Models:
Rohit Singh, Rishabh Singh, Zhilei Xu, Rebecca Krosnick and Armando
Solar-Lezama.
14:00 Synthesis with Identifiers:
Rüdiger Ehlers, Sanjit A. Seshia and Hadas Kress-Gazit.
14:30 Synthesis for Polynomial Lasso Programs:
Jan Leike and Ashish Tiwari.
15:00-15:30 Break
15:30-16:30 Session 12: Abstract interpretation
(Chair: Patrick Cousot)
15:30 Widening for Control-Flow:
Ben Hardekopf, Ben Wiedermann, Berkeley Churchill and Vineeth
Kashyap.
16:00 Policy Iteration-based Conditional Termination and Ranking Functions:
Damien Massé.
16:30 Closing remarks