TACAS 2015 programme

Monday 13 April
10h30 - 12h30 Hybrid systems (Chair: Cesare Tinelli)
  • 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
  • Fabian Immler. Verified Reachability Analysis of Continuous Systems
  • Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta. HYCOMP - an SMT-based model checker for hybrid systems
  • Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan and Matthew Potok. C2E2: A Verification Tool For Annotated Stateflow Models
14h00 - 16h00 Program analysis (Chair: Heike Wehrheim)
  • Elvira Albert, Jesús Correas Fernández and Guillermo Román-Díez. Non-Cumulative Resource Analysis
  • Shrawan Kumar, Amitabha Sanyal and Uday Khedker. Value Slice: A New Slicing Concept for Scalable Property Checking
  • Reng Zeng, Zhuo Sun, Su Liu and Xudong He. A Method for Improving the Precision and Coverage of Atomicity Violation Predictions
  • Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha and Bow-Yaw Wang. Commutativity of Reducers
16h30 - 17h30 Verification, abstraction (Chair: Marsha Chechik)
  • Hiroshi Unno and Tachio Terauchi. Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling
  • Kedar Namjoshi and Richard Trefler. Analysis of Dynamic Process Networks
Tuesday 14 April
14h00 - 16h15 Tool demonstrations (Chair: Jaco van de Pol)
  • Tomas Brazdil, Krishnendu Chatterjee, Vojtech Forejt and Antonin Kucera. MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives
  • Ramiro Demasi, Nicolas Ricci, Pablo Castro, Tom Maibaum and Nazareno Aguirre. syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications
  • Nikolaj Bjorner, Anh-Dung Phan and Lars Fleckenstein. νZ - An Optimizing SMT Solver
  • Soonho Kong, Sicun Gao, Wei Chen and Edmund Clarke. dReach: Delta-Reachability Analysis for Hybrid Systems
  • Alexandre David, Peter G. Jensen, Kim G. Larsen, Marius Mikucionis and Jakob H. Taankvist. STRATEGO: Verification, Performance Analysis and Optimization of Timed Game Strategies
  • Adel Djoudi and Sébastien Bardin. BINSEC: Binary-level analysis with Low-Level Regions
  • Emmanuel Fleury, Olivier Ly, Gérald Point and Aymeric Vincent. Insight: An Open Binary Analysis Framework
  • Gabriele Costa, Alessandro Armando, Alessio Merlo, Gabriele De Maglie, Gianluca Bocci, Giantonio Chiarelli and Rocco Mammoliti. SAM: the Static Analysis Module of the MAVERIC Mobile App Security Verification Platform
  • Yann Thierry-Mieg. Symbolic model-checking using ITS-Tools
16h30 - 18h00 Tool demo market (Chair: Jaco van de Pol)
Wednesday 15 April
9h00 - 10h00 Invited Talk (Chair: Christel Baier)
Wang Yi.
10h30 - 12h00 Stochastic models (Chair: Arie Gurfunkel)
  • Jeffery Hansen, Lutz Wrage, Sagar Chaki, Dionisio De Niz and Mark Klein. Semantic Importance Sampling for Statistical Model Checking
  • Parosh Nicolas Basset, Marta Kwiatkowska, Ufuk Topcu and Clemens Wiltsche. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives
  • Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts and Alessandro Abate. FAUST2: Formal Abstractions of Uncountable-STate STochastic processes
14h00 - 16h00 SAT and SMT (Chair: Tobias Nipkow)
  • Jeroen Bransen, L. Thomas van Binsbergen, Koen Claessen and Atze Dijkstra. Linearly Ordered Attribute Grammar scheduling using SAT-solving
  • Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia and Moshe Y. Vardi. On Parallel Scalable Uniform SAT Witness Generation
  • Dmitry Chistikov, Rayna Dimitrova and Rupak Majumdar. Approximate Counting in SMT and Value Estimation for Probabilistic Programs
  • Roberto Sebastiani and Patrick Trentin. Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
16h30 - 18h00 Partial order reduction, bisimulation and fairness (Chair: Leonore Zuck)
  • Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson and Konstantinos Sagonas. Stateless Model Checking for TSO and PSO
  • Anton Wijs. GPU Accelerated Strong and Branching Bisimulation Checking
  • Byron Cook, Heidy Khlaaf and Nir Piterman. Fairness for Infinite-State Systems
Thursday 16 April
10h30 - 12h30 [SV-COMP talks] (Chair: Dirk Beyer)
15h00 - 16h00 Parameter synthesis (Chair: Joost-Pieter Katoen)
  • Mirco Giacobbe, Calin Guet, Ashutosh Gupta, Thomas Henzinger, Tiago Paixao and Tatjana Petrov. Model Checking Gene Regulatory Networks
  • Ocan Sankur. Symbolic Quantitative Robustness Analysis of Timed Automata
16h30 - 18h00 Program synthesis (Chair: Tiziana Margaria)
  • Rajeev Alur, Salar Moarref and Ufuk Topcu. Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
  • 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
Friday 17 April
10h30 - 12h30 Program and runtime verification (Chair: Christel Baier)
  • 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
  • Adrian Francalanza and Clare Cini. An LTL Proof System for Runtime Verification
  • Giles Reger, Helena Cuenca Cruz and David Rydeheard. MarQ: Monitoring At Runtime with QEA
14h00 - 16h00 Temporal logic and automata (Chair: Christel Baier)
  • Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon and Denis Poitrenaud. Parallel Explicit Model Checking for Generalized Büchi Automata
  • Dileep Kini and Mahesh Viswanathan. Probabilistic Büchi Automata for LTL\GU
  • Vince Molnár, Dániel Darvas, András Vörös and Tamás Bartha. Saturation-based Incremental LTL Model Checking with Inductive Proofs
  • Tomas Fiedor, Lukas Holik, Ondrej Lengal and Tomas Vojnar. Nested Antichains for WS1S
16h30 - 18h00 Model checking (Chair: Cesare Tinelli)
  • Tom van Dijk and Jaco van de Pol. Sylvan: Multi-core Decision Diagrams
  • Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom and Tom van Dijk. LTSmin: High-Performance Language-Independent Model Checking
  • Abderahman Kriouile and Wendelin Serwe. Using a Formal Model to Improve Verification of a Cache Coherent System-on-Chip

Who's online

We have 59 guests and no members online

Site Hosted by