TACAS 2016

69 papers

1. 2LS for Program Analysis - (Competition Contribution) · Peter Schrammel, Daniel Kroening
2. Abstract Learning Frameworks for Synthesis · Christof Löding, P. Madhusudan, Daniel Neider
3. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems · Radu Iosif, Adam Rogalewicz, Tomás Vojnar
4. Acceleration in Multi-PushDown Systems · Mohamed Faouzi Atig, K. Narayan Kumar, Prakash Saivasan
5. Advances in Symbolic Probabilistic Model Checking with PRISM · Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz + 2 more
6. An Automaton Learning Approach to Solving Safety Games over Infinite Graphs · Daniel Neider, Ufuk Topcu
7. An O(m\log n) Algorithm for Stuttering Equivalence and Branching Bisimulation · Jan Friso Groote, Anton Wijs
8. Approaching the Coverability Problem Continuously · Michael Blondin, Alain Finkel, Christoph Haase, Serge Haddad
9. Bit-Vector Optimization · Alexander Nadel, Vadim Ryvchin
10. CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution) · Manchun Zheng, John G. Edenhofner, Ziqing Luo, Mitchell J. Gerrard, Michael S. Rogers, Matthew B. Dwyer + 1 more
11. CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis - (Competition Contribution) · Karlheinz Friedberger
12. CPA-RefSel: CPAchecker with Refinement Selection - (Competition Contribution) · Stefan Löwe
13. Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-Sensitive Business Processes · Luca Compagna, Daniel Ricardo dos Santos, Serena Elisa Ponta, Silvio Ranise
14. Characteristic Formulae for Session Types · Julien Lange, Nobuko Yoshida
15. Complementing Semi-deterministic Büchi Automata · Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai
16. Coqoon - An IDE for Interactive Proof Development in Coq · Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
17. DIVINE: Explicit-State LTL Model Checker - (Competition Contribution) · Vladimír Still, Petr Rockai, Jiri Barnat
18. DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation · Hugues Evrard
19. Deductive Proofs of Almost Sure Persistence and Recurrence Properties · Aleksandar Chakarov, Yuen-Lam Voronin, Sriram Sankaranarayanan
20. Developing and Debugging Proof Strategies by Tinkering · Yuhui Lin, Pierre Le Bras, Gudmund Grov
21. Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets) · Cédric Favre, Hagen Völzer, Peter Müller
22. Efficient Syntax-Driven Lumping of Differential Equations · Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin
23. FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals · Radu Calinescu, Kenneth Johnson, Colin Paterson
24. Faster Statistical Model Checking for Unbounded Temporal Properties · Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
25. Finding Recurrent Sets with Backward Analysis and Trace Partitioning · Alexey Bakhirkin, Nir Piterman
26. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models · Daniel Poetzl, Daniel Kroening
27. Hunting Memory Bugs in C Programs with Map2Check - (Competition Contribution) · Herbert O. Rocha, Raimundo S. Barreto, Lucas C. Cordeiro
28. Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics · Nima Roohi, Pavithra Prabhakar, Mahesh Viswanathan
29. Integrated Environment for Diagnosing Verification Errors · Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz
30. Interpolants in Nonlinear Theories Over the Reals · Sicun Gao, Damien Zufferey
31. JDart: A Dynamic Symbolic Analysis Framework · Kasper Søe Luckow, Marko Dimjasevic, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Temesghen Kahsai + 2 more
32. LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution) · Olli Saarikivi, Keijo Heljanko
33. LPI: Software Verification with Local Policy Iteration - (Competition Contribution) · Egor George Karpenkov
34. MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution) · Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
35. Multi-core Symbolic Bisimulation Minimisation · Tom van Dijk, Jaco van de Pol
36. On Atomicity in Presence of Non-atomic Writes · Constantin Enea, Azadeh Farzan
37. Online Timed Pattern Matching Using Derivatives · Dogan Ulus, Thomas Ferrère, Eugene Asarin, Oded Maler
38. Online and Compositional Learning of Controllers with Application to Floor Heating · Kim G. Larsen, Marius Mikucionis, Marco Muñiz, Jirí Srba, Jakob Haahr Taankvist
39. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark - (Competition Contribution) · Michal Kotoun, Petr Peringer, Veronika Soková, Tomás Vojnar
40. PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games · Marta Kwiatkowska, David Parker, Clemens Wiltsche
41. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems · Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim, Marta Z. Kwiatkowska
42. PTIME Computation of Transitive Closures of Octagonal Relations · Filip Konecný
43. Parameterized Compositional Model Checking · Kedar S. Namjoshi, Richard J. Trefler
44. Parametric Runtime Verification of C Programs · Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang
45. Partial Order Reduction for Event-Driven Multi-threaded Programs · Pallavi Maiya, Rahul Gupta, Aditya Kanade, Rupak Majumdar
46. PrDK: Protocol Programming with Automata · Sung-Shik T. Q. Jongmans, Farhad Arbab
47. Probabilistic CTL*: The Deductive Way · Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns, Rupak Majumdar
48. RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems · Souha Ben Rayana, Marius Bozga, Saddek Bensalem, Jacques Combaz
49. Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication · Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu
50. Reduction of Nondeterministic Tree Automata · Ricardo Almeida, Lukás Holík, Richard Mayr
51. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016) · Dirk Beyer
52. Robots at the Edge of the Cloud · Rupak Majumdar
53. Run Forester, Run Backwards! - (Competition Contribution) · Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar
54. Runtime Monitoring with Union-Find Structures · Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz, Daniel Thoma
55. Safety Verification of Continuous-Space Pure Jump Markov Processes · Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, Alessandro Abate
56. Safety-Constrained Reinforcement Learning for MDPs · Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen
57. Scalable Verification of Linear Controller Software · Junkil Park, Miroslav Pajic, Insup Lee, Oleg Sokolsky
58. Some Complexity Results for Stateful Network Verification · Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker + 1 more
59. Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution) · Marek Chalupa, Martin Jonás, Jiri Slaby, Jan Strejcek, Martina Vitovská
60. Synthesizing Piece-Wise Functions by Learning Classifiers · Daniel Neider, Shambwaditya Saha, P. Madhusudan
61. Synthesizing Ranking Functions from Bits and Pieces · Caterina Urban, Arie Gurfinkel, Temesghen Kahsai
62. T2: Temporal Property Verification · Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman
63. Tactics for the Dafny Program Verifier · Gudmund Grov, Vytautas Tumas
64. TcT: Tyrolean Complexity Tool · Martin Avanzini, Georg Moser, Michael Schaper
65. The xSAP Safety Analysis Platform · Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio + 3 more
66. Ultimate Automizer with Two-track Proofs - (Competition Contribution) · Matthias Heizmann, Daniel Dietsch, Marius Greitschus, Jan Leike, Betim Musa, Claus Schätzle + 1 more
67. Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities · Olivier Bouissou, Eric Goubault, Sylvie Putot, Aleksandar Chakarov, Sriram Sankaranarayanan
68. Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution) · Henning Günther, Alfons Laarman, Georg Weissenbacher
69. v2c - A Verilog to C Translator · Rajdeep Mukherjee, Michael Tautschnig, Daniel Kroening