TACAS 2015 accepted papers

  • Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson and Konstantinos Sagonas. Stateless model checking for TSO and PSO
  • Elvira Albert, Jesús Correas Fernández and Guillermo Román-Díez. Non-cumulative resource analysis
  • Rajeev Alur, Salar Moarref and Ufuk Topcu. Pattern-based refinement of interface specifications in reactive synthesis
  • Parosh Nicolas Basset, Marta Kwiatkowska, Ufuk Topcu and Clemens Wiltsche. Strategy synthesis for stochastic games with multiple long-run objectives
  • Nikolaj Bjorner, Anh-Dung Phan and Lars Fleckenstein. nuZ - an optimizing SMT solver
  • Roderick Bloem, Krishnendu Chatterjee, Swen Jacobs and Robert Koenighofer. Assume-guarantee synthesis for concurrent reactive programs with partial information
  • Roderick Bloem, Bettina Konighofer, Robert Konighofer and Chao Wang. Shield synthesis: runtime enforcement for reactive systems
  • Stefan Blom, Tom van Dijk, Gijs Kant, Alfons Laarman, Jeroen Meijer and Jaco van de Pol. LTSmin: High-performance, language-independent model checking
  • Jeroen Bransen, L. Thomas van Binsbergen, Koen Claessen and Atze Dijkstra. Linearly ordered attribute grammar scheduling using SAT-solving
  • Tomas Brazdil, Krishnendu Chatterjee, Vojtech Forejt and Antonin Kucera. MultiGain: a controller synthesis tool for MDPs with multiple mean-payoff objectives
  • Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia and Moshe Y. Vardi. On parallel scalable uniform SAT witness generation
  • Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha and Bow-Yaw Wang. Commutativity of reducers
  • Dmitry Chistikov, Rayna Dimitrova and Rupak Majumdar. Approximate counting in SMT and Value estimation for probabilistic programs
  • Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta. HYCOMP - an SMT-based model checker for hybrid systems
  • Byron Cook, Heidy Khlaaf and Nir Piterman. Fairness for infinite-state systems
  • Gabriele Costa, Alessandro Armando, Alessio Merlo, Gabriele De Maglie, Gianluca Bocci, Giantonio Chiarelli and Rocco Mammoliti. Mobile app security analysis with the MAVERIC static analysis module
  • Alexandre David, Peter G. Jensen, Kim G. Larsen, Marius Mikucionis and Jakob H. Taankvist. STRATEGO: verification, performance analysis and optimization of timed game strategies
  • Ramiro Demasi, Nicolas Ricci, Pablo Castro, Tom Maibaum and Nazareno Aguirre. syntMaskFT: a tool for synthesizing masking fault-tolerant programs from deontic specifications
  • Adel Djoudi and Sébastien Bardin. BINSEC: Binary-level analysis with low-level regions
  • Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan and Matthew Potok. C2E2: a verification tool for annotated stateflow models
  • Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts and Alessandro Abate. FAUST^2: formal abstractions of uncountable-state stochastic processes
  • Tomas Fiedor, Lukas Holik, Ondrej Lengal and Tomas Vojnar. Nested antichains for WS1S
  • Emmanuel Fleury, Olivier Ly, Gérald Point and Aymeric Vincent. Insight: an open binary analysis framework
  • Adrian Francalanza and Clare Cini. An LTL proof system for runtime verification
  • Jeffery Hansen, Lutz Wrage, Sagar Chaki, Dionisio De Niz and Mark Klein. Semantic importance sampling for statistical model checking
  • Fabian Immler. Verified reachability analysis of continuous systems
  • Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki and André Platzer. A formally verified hybrid system for the next-generation airborne collision avoidance system
  • Dileep Kini and Mahesh Viswanathan. Probabilistic Büchi automata for LTL\GU.
  • Soonho Kong, Sicun Gao, Wei Chen and Edmund Clarke. dReach: delta-reachability analysis for hybrid systems
  • Abderahman Kriouile and Wendelin Serwe. Using a formal model to improve verification of a cache coherent system-on-chip
  • Shrawan Kumar, Amitabha Sanyal and Uday Khedker. Value Slice: A new slicing concept for scalable property checking
  • Vince Molnár, Dániel Darvas, András Vörös and Tamas Bartha. Saturation-based incremental LTL model checking with inductive proofs
  • Kedar Namjoshi and Richard Trefler. Analysis of dynamic process networks
  • Mirco Giacobbe, Calin Guet, Ashutosh Gupta, Thomas Henzinger, Tiago Paixao and Tatjana Petrov. Model checking gene regulatory networks
  • Giles Reger, Helena Cuenca Cruz and David Rydeheard. MarQ: monitoring at runtime with QEA
  • Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon and Denis Poitrenaud. Parallel explicit model checking for generalized Büchi automata
  • Ocan Sankur. Symbolic quantitative robustness analysis of timed automata
  • Roberto Sebastiani and Patrick Trentin. Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions
  • Yann Thierry-Mieg. Symbolic model-checking using ITS-tools
  • Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre and Gennaro Parlato. Verifying concurrent programs by memory unwinding
  • Julian Tschannen, Carlo A. Furia, Martin Nordio and Nadia Polikarpova. AutoProof: Auto-active functional verification of object-oriented programs
  • Hiroshi Unno and Tachio Terauchi. Inferring simple solutions to recursion-free Horn clauses via sampling
  • Tom van Dijk and Jaco Van De Pol. Sylvan: multi-core decision diagrams
  • Anton Wijs. GPU accelerated strong and branching bisimulation checking
  • Reng Zeng, Zhuo Sun, Su Liu and Xudong He. A method for improving the precision and coverage of atomicity violation predictions