TACAS 2015

62 papers

1. A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System · Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki + 1 more
2. A Method for Improving the Precision and Coverage of Atomicity Violation Predictions · Reng Zeng, Zhuo Sun, Su Liu, Xudong He
3. AProVE: Termination and Memory Safety of C Programs - (Competition Contribution) · Thomas Ströder, Cornelius Aschermann, Florian Frohn, Jera Hensel, Jürgen Giesl
4. An LTL Proof System for Runtime Verification · Clare Cini, Adrian Francalanza
5. Analysis of Dynamic Process Networks · Kedar S. Namjoshi, Richard J. Trefler
6. Approximate Counting in SMT and Value Estimation for Probabilistic Programs · Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar
7. Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information · Roderick Bloem, Krishnendu Chatterjee, Swen Jacobs, Robert Könighofer
8. AutoProof: Auto-Active Functional Verification of Object-Oriented Programs · Julian Tschannen, Carlo A. Furia, Martin Nordio, Nadia Polikarpova
9. BINSEC: Binary Code Analysis with Low-Level Regions · Adel Djoudi, Sébastien Bardin
10. C2E2: A Verification Tool for Stateflow Models · Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, Matthew Potok
11. CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic - (Competition Contribution) · Matthias Dangl, Stefan Löwe, Philipp Wendler
12. CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution) · Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
13. Cascade - (Competition Contribution) · Wei Wang, Clark W. Barrett
14. Commutativity of Reducers · Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, Bow-Yaw Wang
15. FAUST 2 : Formal Abstractions of Uncountable-STate STochastic Processes · Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts, Alessandro Abate
16. Fairness for Infinite-State Systems · Byron Cook, Heidy Khlaaf, Nir Piterman
17. Forester: Shape Analysis Using Tree Automata - (Competition Contribution) · Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar
18. FramewORk for Embedded System verification - (Competition Contribution) · Pablo González de Aledo, Pablo Sánchez Espeso
19. FuncTion: An Abstract Domain Functor for Termination - (Competition Contribution) · Caterina Urban
20. GPU Accelerated Strong and Branching Bisimilarity Checking · Anton Wijs
21. HyComp: An SMT-Based Model Checker for Hybrid Systems · Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
22. Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling · Hiroshi Unno, Tachio Terauchi
23. Insight: An Open Binary Analysis Framework · Emmanuel Fleury, Olivier Ly, Gérald Point, Aymeric Vincent
24. LTSmin: High-Performance Language-Independent Model Checking · Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, Tom van Dijk
25. Limit Deterministic and Probabilistic Automata for LTL ∖ GU · Dileep Kini, Mahesh Viswanathan
26. Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving · Jeroen Bransen, L. Thomas van Binsbergen, Koen Claessen, Atze Dijkstra
27. MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution) · Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
28. MarQ: Monitoring at Runtime with QEA · Giles Reger, Helena Cuenca Cruz, David E. Rydeheard
29. Model Checking Gene Regulatory Networks · Mirco Giacobbe, Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Tiago Paixão, Tatjana Petrov
30. MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives · Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera
31. Nested Antichains for WS1S · Tomás Fiedor, Lukás Holík, Ondrej Lengál, Tomás Vojnar
32. Non-cumulative Resource Analysis · Elvira Albert, Jesús Correas Fernández, Guillermo Román-Díez
33. On Parallel Scalable Uniform SAT Witness Generation · Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi
34. Parallel Explicit Model Checking for Generalized Büchi Automata · Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud
35. Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis · Rajeev Alur, Salar Moarref, Ufuk Topcu
36. Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution) · Franck Cassez, Takashi Matsuoka, Edward Pierzchalski, Nathan Smyth
37. Predator Hunting Party (Competition Contribution) · Petr Müller, Petr Peringer, Tomás Vojnar
38. Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions · Roberto Sebastiani, Patrick Trentin
39. SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform · Alessandro Armando, Gianluca Bocci, Giantonio Chiarelli, Gabriele Costa, Gabriele De Maglie, Rocco Mammoliti + 1 more
40. SMACK+Corral: A Modular Verifier - (Competition Contribution) · Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric
41. Saturation-Based Incremental LTL Model Checking with Inductive Proofs · Vince Molnár, Dániel Darvas, András Vörös, Tamás Bartha
42. Scalable Timing Analysis with Refinement · Nan Guan, Yue Tang, Jakaria Abdullah, Martin Stigge, Wang Yi
43. SeaHorn: A Framework for Verifying C Programs (Competition Contribution) · Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas
44. Semantic Importance Sampling for Statistical Model Checking · Jeffery P. Hansen, Lutz Wrage, Sagar Chaki, Dionisio de Niz, Mark H. Klein
45. Shield Synthesis: - Runtime Enforcement for Reactive Systems · Roderick Bloem, Bettina Könighofer, Robert Könighofer, Chao Wang
46. Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015) · Dirk Beyer
47. Stateless Model Checking for TSO and PSO · Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, Konstantinos Sagonas
48. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives · Nicolas Basset, Marta Z. Kwiatkowska, Ufuk Topcu, Clemens Wiltsche
49. Sylvan: Multi-Core Decision Diagrams · Tom van Dijk, Jaco van de Pol
50. Symbolic Model-Checking Using ITS-Tools · Yann Thierry-Mieg
51. Symbolic Quantitative Robustness Analysis of Timed Automata · Ocan Sankur
52. ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution) · Alexander Nutz, Daniel Dietsch, Mostafa Mahmoud Mohamed, Andreas Podelski
53. Ultimate Automizer with Array Interpolation - (Competition Contribution) · Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa, Andreas Podelski
54. Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution) · Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
55. Uppaal Stratego · Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikucionis, Jakob Haahr Taankvist
56. Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip · Abderahman Kriouile, Wendelin Serwe
57. Value Slice: A New Slicing Concept for Scalable Property Checking · Shrawan Kumar, Amitabha Sanyal, Uday P. Khedker
58. Verified Reachability Analysis of Continuous Systems · Fabian Immler
59. Verifying Concurrent Programs by Memory Unwinding · Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
60. dReach: δ-Reachability Analysis for Hybrid Systems · Soonho Kong, Sicun Gao, Wei Chen, Edmund M. Clarke
61. syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications · Ramiro Demasi, Pablo F. Castro, Nicolás Ricci, Thomas Stephen Edward Maibaum, Nazareno Aguirre
62. νZ - An Optimizing SMT Solver · Nikolaj S. Bjørner, Anh-Dung Phan, Lars Fleckenstein