TACAS 2019

73 papers

1. Abstract Dependency Graphs and Their Application to Model Checking · Søren Enevoldsen, Kim Guldstrand Larsen, Jirí Srba
2. Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude · Si Liu, Peter Csaba Ölveczky, Min Zhang, Qi Wang, José Meseguer
3. Automatic Verification of C and Java Programs: SV-COMP 2019 · Dirk Beyer
4. Binary Decision Diagrams with Edge-Specified Reductions · Junaid Babar, Chuan Jiang, Gianfranco Ciardo, Andrew S. Miner
5. Building Better Bit-Blasting for Floating-Point Problems · Martin Brain, Florian Schanda, Youcheng Sun
6. CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker - (Competition Contribution) · Kareem Khazem, Michael Tautschnig
7. COMPASS 3.0 · Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta
8. Checking Deadlock-Freedom of Parametric Component-Based Systems · Marius Bozga, Radu Iosif, Joseph Sifakis
9. Computing Coupled Similarity · Benjamin Bisping, Uwe Nestmann
10. Computing the Expected Execution Time of Probabilistic Workflow Nets · Philipp J. Meyer, Javier Esparza, Philip Offtermatt
11. Confluence Competition 2019 · Aart Middeldorp, Julian Nagele, Kiraku Shintani
12. Constraint-Based Monitoring of Hyperproperties · Christopher Hahn, Marvin Stenger, Leander Tentrup
13. Debugging of Behavioural Models with CLEAR · Gianluca Barbon, Vincent Leroy, Gwen Salaün
14. Decomposing Farkas Interpolants · Martin Blicha, Antti E. J. Hyvärinen, Jan Kofron, Natasha Sharygina
15. Digital Bifurcation Analysis of TCP Dynamics · Nikola Benes, Lubos Brim, Samuel Pastva, David Safránek
16. ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution) · Mikhail Y. R. Gadelha, Felipe R. Monteiro, Lucas C. Cordeiro, Denis A. Nicole
17. Effective Entailment Checking for Separation Logic with Inductive Definitions · Jens Katelaan, Christoph Matheja, Florian Zuleger
18. Encoding Redundancy for Satisfaction-Driven Clause Learning · Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
19. Environmentally-Friendly GR(1) Synthesis · Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck
20. Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution) · Henrich Lauko, Vladimír Still, Petr Rockai, Jiri Barnat
21. Extending a Brainiac Prover to Lambda-Free Higher-Order Logic · Petar Vukmirovic, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz
22. ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions · Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik
23. Incremental Analysis of Evolving Alloy Models · Wenxi Wang, Kaiyuan Wang, Milos Gligoric, Sarfraz Khurshid
24. International Competition on Runtime Verification (CRV) · Ezio Bartocci, Yliès Falcone, Giles Reger
25. International Competition on Software Testing (Test-Comp) · Dirk Beyer
26. JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution) · Lucas C. Cordeiro, Daniel Kroening, Peter Schrammel
27. Java Pathfinder at SV-COMP 2019 (Competition Contribution) · Cyrille Artho, Willem Visser
28. JayHorn: A Java Model Checker - (Competition Contribution) · Temesghen Kahsai, Philipp Rümmer, Martin Schäf
29. LCV: A Verification Tool for Linear Controller Software · Junkil Park, Miroslav Pajic, Oleg Sokolsky, Insup Lee
30. Measuring Masking Fault-Tolerance · Pablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi, Luciano Putruele
31. MetAcsl: Specification and Verification of High-Level Properties · Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
32. Minimal-Time Synthesis for Parametric Timed Automata · Étienne André, Vincent Bloemen, Laure Petrucci, Jaco van de Pol
33. Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework · Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon
34. Multi-core On-The-Fly Saturation · Tom van Dijk, Jeroen Meijer, Jaco van de Pol
35. Omega-Regular Objectives in Model-Free Reinforcement Learning · Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
36. On Reachability in Parameterized Phaser Programs · Zeinab Ganjei, Ahmed Rezine, Ludovic Henrio, Petru Eles, Zebo Peng
37. On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Transition · Thomas Bläsius, Tobias Friedrich, Andrew M. Sutton
38. Optimal Time-Bounded Reachability Analysis for Concurrent Systems · Yuliya Butkova, Gereon Fox
39. Parallel SAT Simplification on GPU Architectures · Muhammad Osama, Anton Wijs
40. PeSCo: Predicting Sequential Combinations of Verifiers - (Competition Contribution) · Cedric Richter, Heike Wehrheim
41. PhASAR: An Inter-procedural Static Analysis Framework for C/C++ · Philipp Dominik Schubert, Ben Hermann, Eric Bodden
42. Pinaka: Symbolic Execution Meets Incremental Solving - (Competition Contribution) · Eti Chaudhary, Saurabh Joshi
43. Presentation of the 9th Edition of the Model Checking Contest · Elvio Gilberto Amparore, Bernard Berthomieu, Gianfranco Ciardo, Silvano Dal-Zilio, Francesco Gallà, Lom-Messan Hillah + 13 more
44. Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks · Pengfei Gao, Hongyi Xie, Jun Zhang, Fu Song, Taolue Chen
45. RERS 2019: Combining Synthesis with Real-World Models · Marc Jasper, Malte Mues, Alnis Murtovi, Maximilian Schlüter, Falk Howar, Bernhard Steffen + 5 more
46. ROLL 1.0: \omega -Regular Language Learning Library · Yong Li, Xuechao Sun, Andrea Turrini, Yu-Fang Chen, Junnan Xu
47. Reachability Analysis for Termination and Confluence of Rewriting · Christian Sternagel, Akihisa Yamada
48. SL-COMP: Competition of Solvers for Separation Logic · Mihaela Sighireanu, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds + 18 more
49. Semantic Fault Localization and Suspiciousness Ranking · Maria Christakis, Matthias Heizmann, Muhammad Numair Mansur, Christian Schilling, Valentin Wüstholz
50. Shepherding Hordes of Markov Chains · Milan Ceska, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen
51. Specification and Efficient Monitoring Beyond STL · Alexey Bakhirkin, Nicolas Basset
52. Symbolic Pathfinder for SV-COMP - (Competition Contribution) · Yannic Noller, Corina S. Pasareanu, Aymeric Fromherz, Xuan-Bach Dinh Le, Willem Visser
53. Symbolic Regex Matcher · Olli Saarikivi, Margus Veanes, Tiki Wan, Eric Xu
54. Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach · Mahmoud Khaled, Eric S. Kim, Murat Arcak, Majid Zamani
55. TOOLympics 2019: An Overview of Competitions in Formal Methods · Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns + 9 more
56. Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments · Satoshi Kura, Natsuki Urabe, Ichiro Hasuo
57. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report) · Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Kretínský + 4 more
58. The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations · Nils Becker, Peter Müller, Alexander J. Summers
59. The Quantitative Verification Benchmark Set · Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, Enno Ruijters
60. The Rewrite Engines Competitions: A RECtrospective · Francisco Durán, Hubert Garavel
61. The Termination and Complexity Competition · Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
62. The mCRL2 Toolset for Analysing Concurrent Systems - Improvements in Expressivity and Usability · Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink + 3 more
63. VIAP 1.1 - (Competition Contribution) · Pritom Rajkhowa, Fangzhen Lin
64. VeriFuzz: Program Aware Fuzzing - (Competition Contribution) · Animesh Basak Chowdhury, Raveendra Kumar Medicherla, R. Venkatesh
65. Verifiably Safe Off-Model Reinforcement Learning · Nathan Fulton, André Platzer
66. VerifyThis - Verification Competition with a Human Factor · Gidon Ernst, Marieke Huisman, Wojciech Mostowski, Mattias Ulbrich
67. Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking · Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
68. VoxLogicA: A Spatial Model Checker for Declarative Image Analysis · Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink
69. VyPR2: A Framework for Runtime Verification of Python Web Services · Joshua Heneage Dawes, Giles Reger, Giovanni Franzoni, Andreas Pfeiffer, Giacomo Govi
70. WAPS: Weighted and Projected Sampling · Rahul Gupta, Shubham Sharma, Subhajit Roy, Kuldeep S. Meel
71. \mathsf StocHy : Automated Verification and Synthesis of Stochastic Processes · Nathalie Cauchi, Alessandro Abate
72. i _\mathrm Rank : A Variable Order Metric for DEDS Subject to Linear Invariants · Elvio Gilberto Amparore, Gianfranco Ciardo, Susanna Donatelli, Andrew S. Miner
73. nonreach - A Tool for Nonreachability Analysis · Florian Meßner, Christian Sternagel