TACAS 2014

55 papers

1. APTE: An Algorithm for Proving Trace Equivalence · Vincent Cheval
2. Alternating Runtime and Size Complexity Analysis of Integer Programs · Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl
3. Analyzing the Next Generation Airborne Collision Avoidance System · Christian von Essen, Dimitra Giannakopoulou
4. Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata · Ting Wang, Jun Sun, Yang Liu, Xinyu Wang, Shanping Li
5. Basic Problems in Multi-View Modeling · Jan Reineke, Stavros Tripakis
6. Bounds2: A Tool for Compositional Multi-parametrised Verification · Antti Siirtola
7. CBMC - C Bounded Model Checker - (Competition Contribution) · Daniel Kroening, Michael Tautschnig
8. CIF 3: Model-Based Engineering of Supervisory Controllers · D. A. van Beek, Wan J. Fokkink, Dennis Hendriks, Albert T. Hofkamp, Jasen Markovski, Joanna M. van de Mortel-Fronczak + 1 more
9. CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution) · Stefan Löwe, Mikhail U. Mandrykin, Philipp Wendler
10. CPAlien: Shape Analyzer for CPAChecker - (Competition Contribution) · Petr Müller, Tomás Vojnar
11. Characterizing Algebraic Invariants by Differential Radical Invariants · Khalil Ghorbal, André Platzer
12. Compositional Invariant Generation for Timed Systems · Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz
13. Computing Conditional Probabilities in Markovian Models Efficiently · Christel Baier, Joachim Klein, Sascha Klüppelholz, Steffen Märcker
14. Concurrent Depth-First Search Algorithms · Gavin Lowe
15. Decision Procedures for Flat Array Properties · Francesco Alberti, Silvio Ghilardi, Natasha Sharygina
16. Detecting Unrealizable Specifications of Distributed Systems · Bernd Finkbeiner, Leander Tentrup
17. Discounting in LTL · Shaull Almagor, Udi Boker, Orna Kupferman
18. EDD: A Declarative Debugger for Sequential Erlang Programs · Rafael Caballero, Enrique Martin-Martin, Adrián Riesco, Salvador Tamarit
19. ESBMC 1.22 - (Competition Contribution) · Jeremy Morse, Mikhail Ramalho, Lucas C. Cordeiro, Denis A. Nicole, Bernd Fischer
20. Environment-Model Based Testing of Control Systems: Case Studies · Erwan Jahier, Simplice Djoko Djoko, Chaouki Maiza, Eric Lafont
21. FDR3 - A Modern Refinement Checker for CSP · Thomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, A. W. Roscoe
22. Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic · Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta
23. Forward Reachability Computation for Autonomous Max-Plus-Linear Systems · Dieky Adzkiya, Bart De Schutter, Alessandro Abate
24. FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution) · Arie Gurfinkel, Anton Belov
25. GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs · Anton Wijs, Dragan Bosnacki
26. GRASShopper - Complete Heap Verification with Mixed Specifications · Ruzica Piskac, Thomas Wies, Damien Zufferey
27. IC3 Modulo Theories via Implicit Predicate Abstraction · Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
28. Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution) · Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
29. Learning Regular Languages over Large Alphabets · Oded Maler, Irini-Eleftheria Mens
30. MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution) · Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato
31. Monitoring Modulo Theories · Normann Decker, Martin Leucker, Daniel Thoma
32. On the Correctness of a Branch Displacement Algorithm · Jaap Boender, Claudio Sacerdoti Coen
33. PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence · Michael Huth, Jim Huan-Pu Kuo
34. Permissive Controller Synthesis for Probabilistic Systems · Klaus Dräger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma
35. Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance · Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate
36. Predator: A Shape Analyzer Based on Symbolic Memory Graphs - (Competition Contribution) · Kamil Dudka, Petr Peringer, Tomás Vojnar
37. Proving Nontermination via Safety · Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn
38. Quasi-Equal Clock Reduction: More Networks, More Queries · Christian Herrera, Bernd Westphal, Andreas Podelski
39. Ranking Templates for Linear Loops · Jan Leike, Matthias Heizmann
40. SACO: Static Analyzer for Concurrent Objects · Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin + 2 more
41. SATMC: A SAT-Based Model Checker for Security-Critical Systems · Alessandro Armando, Roberto Carbone, Luca Compagna
42. SMT-Based Verification of Software Countermeasures against Side-Channel Attacks · Hassan Eldib, Chao Wang, Patrick Schaumont
43. Status Report on Software Verification - (Competition Summary SV-COMP 2014) · Dirk Beyer
44. Symbiotic 2: More Precise Slicing - (Competition Contribution) · Jiri Slaby, Jan Strejcek
45. Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata · Ala-Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg
46. Symbolic Synthesis for Epistemic Specifications with Observational Semantics · Xiaowei Huang, Ron van der Meyden
47. Synthesis for Human-in-the-Loop Control Systems · Wenchao Li, Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia
48. Synthesizing Safe Bit-Precise Invariants · Arie Gurfinkel, Anton Belov, João Marques-Silva
49. Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems · Thomas Reinbacher, Kristin Yvonne Rozier, Johann Schumann
50. The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification · Arnd Hartmanns, Holger Hermanns
51. Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution) · Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa + 3 more
52. Ultimate Kojak - (Competition Contribution) · Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, Andreas Podelski
53. Variations on Safety · Orna Kupferman
54. VeriMAP: A Tool for Verifying Programs through Transformations · Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
55. Verification of Concurrent Quantum Protocols by Equivalence Checking · Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan