TACAS 2020

60 papers

1. 2LS: Heap Analysis and Memory Safety - (Competition Contribution) · Viktor Malík, Peter Schrammel, Tomás Vojnar
2. A Calculus for Modular Loop Acceleration · Florian Frohn
3. A Study of Symmetry Breaking Predicates and Model Counting · Wenxi Wang, Muhammad Usman, Alyas Almaawi, Kaiyuan Wang, Kuldeep S. Meel, Sarfraz Khurshid
4. AVR: Abstractly Verifying Reachability · Aman Goel, Karem A. Sakallah
5. Advances in Automatic Software Verification: SV-COMP 2020 · Dirk Beyer
6. An O(m log n) algorithm for branching bisimilarity on labelled transition systems · David N. Jansen, Jan Friso Groote, Jeroen J. A. Keiren, Anton Wijs
7. Analysing installation scenarios of Debian packages · Benedikt F. H. Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen
8. Assume, Guarantee or Repair · Hadar Frenkel, Orna Grumberg, Corina S. Pasareanu, Sarai Sheinvald
9. Automated Verification of Parallel Nested DFS · Wytse Oortwijn, Marieke Huisman, Sebastiaan J. C. Joosten, Jaco van de Pol
10. Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers · Daniele Ahmed, Andrea Peruffo, Alessandro Abate
11. COASTAL: Combining Concolic and Fuzzing for Java (Competition Contribution) · Willem Visser, Jaco Geldenhuys
12. CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering · Dirk Beyer, Philipp Wendler
13. Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution) · Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer
14. Deciding the Bisimilarity of Context-Free Session Types · Bernardo Almeida, Andreia Mordido, Vasco T. Vasconcelos
15. Describing and Simulating Concurrent Quantum Systems · Richard Bornat, Jaap Boender, Florian Kammueller, Guillaume Poly, Rajagopal Nagarajan
16. Discourje: Runtime Verification of Communication Protocols in Clojure · Ruben Hamers, Sung-Shik Jongmans
17. EMTST: Engineering the Meta-theory of Session Types · David Castro-Perez, Francisco Ferreira, Nobuko Yoshida
18. Endicheck: Dynamic Analysis for Detecting Endianness Bugs · Roman Kápl, Pavel Parízek
19. FIG: The Finite Improbability Generator · Carlos E. Budde
20. Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints · Florian Funke, Simon Jantsch, Christel Baier
21. Fold/Unfold Transformations for Fixpoint Logic · Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta
22. Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting · Alexander Lochmann, Aart Middeldorp
23. GACAL: Conjecture-Based Verification - (Competition Contribution) · Benjamin Quiring, Panagiotis Manolios
24. GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts · Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, Albert Rubio
25. Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning · Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
26. Highly Automated Formal Proofs over Memory Usage of Assembly Code · Freek Verbeek, Joshua A. Bockenek, Binoy Ravindran
27. How Many Bits Does it Take to Quantize Your Neural Network? · Mirco Giacobbe, Thomas A. Henzinger, Mathias Lechner
28. Interpretation-Based Violation Witness Validation for C: NITWIT · Jan Svejda, Philipp Berger, Joost-Pieter Katoen
29. JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contribution) · Malte Mues, Falk Howar
30. Java Ranger at SV-COMP 2020 (Competition Contribution) · Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser
31. KReach: A Tool for Reachability in Petri Nets · Alex Dixon, Ranko Lazic
32. Learning One-Clock Timed Automata · Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang
33. MUST: Minimal Unsatisfiable Subsets Enumeration Tool · Jaroslav Bendík, Ivana Cerná
34. Map2Check: Using Symbolic Execution and Fuzzing - (Competition Contribution) · Herbert Rocha, Rafael Menezes, Lucas C. Cordeiro, Raimundo S. Barreto
35. Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic · Takamasa Okudono, Andy King
36. Mora - Automatic Generation of Moment-Based Invariants · Ezio Bartocci, Laura Kovács, Miroslav Stankovic
37. Multi-agent Safety Verification Using Symmetry Transformations · Hussein Sibai, Navid Mokhlesi, Chuchu Fan, Sayan Mitra
38. Partial Order Reduction for Deep Bug Finding in Synchronous Hardware · Makai Mann, Clark W. Barrett
39. Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems · Thomas Neele, Tim A. C. Willemse, Wieger Wesselink
40. Polynomial Identification of ømega-Automata · Dana Angluin, Dana Fisman, Yaara Shoval
41. Practical Machine-Checked Formalization of Change Impact Analysis · Karl Palmskog, Ahmet Çelik, Milos Gligoric
42. PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution) · Petr Peringer, Veronika Soková, Tomás Vojnar
43. Rare Event Simulation for Non-Markovian Repairable Fault Trees · Carlos E. Budde, Marco Biagi, Raúl E. Monti, Pedro R. D'Argenio, Mariëlle Stoelinga
44. Relational Differential Dynamic Logic · Juraj Kolcák, Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata, David Sprunger, Akihisa Yamada
45. Revisiting Underapproximate Reachability for Multipushdown Systems · S. Akshay, Paul Gastin, S. Krishna, Sparsa Roychowdhury
46. Safe Decomposition of Startup Requirements: Verification and Synthesis · Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly, Stefano Tonetta
47. Scenario-Based Verification of Uncertain MDPs · Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu
48. Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities · Frédéric Lang, Radu Mateescu, Franco Mazzanti
49. Simple Strategies in Multi-Objective MDPs · Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour
50. Software Verification with PDR: An Implementation of the State of the Art · Dirk Beyer, Matthias Dangl
51. Solving Mean-Payoff Games via Quasi Dominions · Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero
52. Structural Invariants for the Verification of Systems with Parameterized Architectures · Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, Christoph Welzel
53. Symbiotic 7: Integration of Predator and More - (Competition Contribution) · Marek Chalupa, Tomás Jasek, Lukás Tomovic, Martin Hruska, Veronika Soková, Paulína Ayaziová + 2 more
54. Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions - (Competition Contribution) · Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Frank Schüssele
55. VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution) · Mohammad Afzal, Supratik Chakraborty, Avriti Chauhan, Bharti Chimdyalwar, Priyanka Darke, Ashutosh Gupta + 4 more
56. Verified Certification of Reachability Checking for Timed Automata · Simon Wimmer, Joshua von Mutius
57. Verifying Array Manipulating Programs with Full-Program Induction · Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat
58. Verifying OpenJDK's LinkedList using KeY · Hans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Marko C. J. D. van Eekelen, Stijn de Gouw
59. Verifying Quantum Communication Protocols with Ground Bisimulation · Xudong Qin, Yuxin Deng, Wenjie Du
60. What's Decidable About Program Verification Modulo Axioms? · Umang Mathur, P. Madhusudan, Mahesh Viswanathan