Program, VMCAI'14, January 19-21, 2013.   
US Grant, San Diego


Sunday, January 19

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