VMCAI 2014 Accepted Papers

Anthony Romano. Practical Floating-Point Tests with Integer Code

Nuno P. Lopes and Jose Monteiro. Weakest Precondition Synthesis for Compiler Optimizations

Martin Schwarz, Helmut Seidl, Vesal Vojdani and Kalmer Apinis. Precise analysis of value-dependent synchronization in programs with priority scheduling

Chao Wang and Kevin Hoang. Deciding Control State Reachability in Concurrent Traces with Limited Observability

Peter Faymonville, Bernd Finkbeiner and Doron Peled. Monitoring Parametric Temporal Logic

Roderick Bloem, Robert Koenighofer and Martina Seidl. SAT-Based Synthesis Methods for Safety Specs

Lei Song, Lijun Zhang and Jens Chr. Godskesen. Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes

Krishnendu Chatterjee, Laurent Doyen, Emmanuel Filiot and Jean-Francois Raskin. Doomsday Equilibria for Omega-Regular Games

Damien Massé. Policy Iteration-based Conditional Termination and Ranking Functions

Andreas Gustavsson, Jan Gustafsson and Björn Lisper. Timing Analysis of Parallel Software Using Abstract Execution

Benjamin Aminof, Swen Jacobs, Ayrat Khalimov and Sasha Rubin. Parameterized Model Checking of Token-Passing Systems

Pietro Ferrara. Generic Combination of Heap and Value Analyses in Abstract Interpretation

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti. Verifying Array Programs by Transforming Verification Conditions

Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder and Damien Zufferey. A Logic-based Framework for Verifying Consensus Algorithms

Antoine Miné. Relational Thread-Modular Static Value Analysis by Abstract Interpretation

Rohit Singh, Rishabh Singh, Zhilei Xu, Rebecca Krosnick and Armando Solar-Lezama. Modular Synthesis of Sketches using Models

Ben Hardekopf, Ben Wiedermann, Berkeley Churchill and Vineeth Kashyap. Widening for Control-Flow

Rüdiger Ehlers, Sanjit A. Seshia and Hadas Kress-Gazit. Synthesis with Identifiers

Jan Leike and Ashish Tiwari. Synthesis for Polynomial Lasso Programs

Dileep Kini and Mahesh Viswanathan. Probabilistic Automata for Safety LTL Specifications

Radu Iosif, Marius Bozga and Filip Konecny. Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops

Vicente Acuña, Andres Aravena, Alejandro Maass and Anne Siegel. Modelling parsimonious putative regulatory networks: complexity and heuristic approaches

Loig Jezequel and Javier Esparza. Message Passing Algorithms for the Verification of Distributed Protocols

Zhoulai Fu. Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java

Wei Wang, Clark Barrett and Thomas Wies. Cascade 2.0 (Tool Paper)