ETAPS 2013: 16-24 March 2013, Rome, Italy

TACAS 2013 accepted papers

You can find information about LNCS proceedings (LNCS 7795) at http://www.springeronline.com/978-3-642-36741-0 or access the online version at http://www.springerlink.com/content/978-3-642-36741-0/.

Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu and Nicholas Smallbone: Encoding Monomorphic and Polymorphic Types

David White and Gerald Lüttgen: Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory

Ebrahim Ardeshir-Larijani, Simon Gay and Rajagopal Nagarajan: Equivalence Checking Quantum Protocols

Siert Wieringa and Keijo Heljanko: Asynchronous Multi-Core Incremental SAT Solving

Yasuhiko Minamide: Weighted Pushdown Systems with Indexed Weight Domains

Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma and Roberto Sebastiani: The MathSAT5 SMT Solver

Radu Mateescu and Gwen Salaün: PIC2LNT: Model Transformation for Model Checking an Applied Pi-calculus

Michael Benedikt, Rastislav Lenhardt and James Worrell: LTL model checking of Interval Markov Chains

Boyang Li, Isil Dillig, Thomas Dillig, Ken Mcmillan and Mooly Sagiv: Synthesis of Circular Compositional Program Proofs via Abduction

Aaron Bohy, Véronique Bruyère, Emmanuel Filiot and Jean-Francois Raskin: Synthesis from LTL Specifications with Mean-Payoff Objectives

Etienne Renault, Fabrice Kordon, Alexandre Duret-Lutz and Denis Poitrenaud: Strength-based decomposition of the property Büchi automaton for faster model-checking

Jean-Francois Kempf, Marius Bozga and Oded Maler: As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty

Patrice Godefroid and Mihalis Yannakakis: Analysis of Boolean Programs

Kshitij Bansal, Eric Koskinen, Thomas Wies and Damien Zufferey: Structural Counter Abstraction

Michael Backes, Sebastian Gerling, Christian Hammer, Matteo Maffei and Philipp von Styp-Rekowsky: AppGuard - Enforcing User Requirements on Android Apps

Fu Song and Tayssir Touili: LTL Model-Checking for Malware Detection

Anton Belov, Matti Järvisalo and Joao Marques-Silva: Formula Preprocessing in MUS Extraction

Anna Lisa Ferrara, P. Madhusudan and Gennaro Parlato: Policy Analysis for Self-Administrated Role-Based Access Control

Robert Nagy, Gerardo Schneider and Aram Timofeitchik: Automatic Testing of Real-Time Graphic Systems

Juergen Christ, Jochen Hoenicke and Alexander Nutz: Proof Tree Preserving Interpolation

Yakir Vizel, Orna Grumberg and Sharon Shoham: Intertwined Forward-Backward Reachability Analysis Using Interpolants

Milos Gligoric and Rupak Majumdar: Model Checking Database Applications

Byron Cook, Abigail See and Florian Zuleger: Ramsey vs. lexicographic termination proving

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen and Radu Mardare: On-the-Fly Exact Computation of Bisimilarity Distances

Ajith John and Supratik Chakraborty: Extending Quantifier Elimination to Linear Inequalities on Bit-vectors

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson and Ahmed Rezine: Memorax: Fence Inference under the TSO Memory Model

Sjoerd Cranen, Jan Friso Groote, Jeroen Keiren, Frank Stappers, Erik de Vink, Wieger Wesselink and Tim Willemse: Ins and outs of the mCRL2 toolset

Sooraj Bhat, Johannes Borgström, Andy Gordon and Claudio Russo: Deriving Probability Density Functions from Probabilistic Functional Programs

Taolue Chen, Vojtech Forejt, Marta Kwiatkowska, David Parker and Aistis Simaitis: PRISM-games: A Model Checker for Stochastic Multi-Player Games

Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen and Nikos Tzevelekos: Runtime Verification Based on Register Automata

Alexander Linden and Pierre Wolper: A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems

Pierre Ganty, Radu Iosif and Filip Konecny: Underapproximation of Procedure Summaries for Integer Programs

Grigory Fedyukovich, Ondrej Sery and Natasha Sharygina: eVolCheck: Incremental Upgrade Checker for C

Anton Wijs and Luc Engelen: Efficient Property Preservation Checking of Model Refinements

Parosh Aziz Abdulla, Frédéric Haziza, Lukas Holik, Bengt Jonsson and Ahmed Rezine: An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

Aleksandra Jovanovic, Didier Lime and Olivier H. Roux: Integer Parameter Synthesis for Timed Automata

Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Sondergaard and Peter Schachte: Unbounded Model-Checking with Interpolation for Regular Language Constraints

Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini and Lijun Zhang: The Quest for Minimal Quotients for Probabilistic Automata

Corina Pasareanu, Daniel Balasubramanian, Gabor Karsai and Michael Lowry: Polyglot: Systematic Analysis for Multiple Statechart Formalisms

Yu-Fang Chen and Bow-Yaw Wang: BULL: a Library for Learning Algorithms of Boolean Functions

Chung-Hao Huang, Sven Schewe and Farn Wang: Model-Checking Iterative Games

Masoud Koleini, Eike Ritter and Mark Ryan: Model checking agent knowledge in dynamic access control policies