TACAS 2018 Accepted Papers
- Giles Reger, Martin Suda and Andrei Voronkov. Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning
- Cristian Mattarei, Clark Barrett, Shu-Yu Guo, Bradley Nelson and Ben Smith. EMME: a formal tool for the ECMAScript Memory Model Evaluation
- Shrawan Kumar, Amitabha Sanyal, Venkatesh R and Punit Shah. Property Checking Array Programs Using Loop Shrinking
- Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker and Robert Bastian. Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper)
- Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns and Sean Sedwards. A Statistical Model Checker for Nondeterminism and Rare Events
- Marijn Heule and Armin Biere. What a Difference a Variable Makes
- Randal Bryant. Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
- Adrien Champion, Tomoya Chiba, Naoki Kobayashi and Ryosuke Sato. ICE-based Refinement Type Discovery for Higher-Order Functional Programs
- Bernd Finkbeiner, Christopher Hahn, Marvin Stenger and Leander Tentrup. RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
- Tomas Brazdil, Krishnendu Chatterjee, Jan Kretinsky and Viktor Toman. Strategy Representation by Decision Trees in Reactive Synthesis
- Dejan Nickovic, Olivier Lebeltel, Oded Maler, Thomas Ferrère and Dogan Ulus. AMT2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic
- Hakan Metin, Souheib Baarir, Maximilien Colange and Fabrice Kordon. CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving
- Iulia Dragomir, Viorel Preoteasa and Stavros Tripakis. The Refinement Calculus of Reactive Systems Toolset
- Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann. Multi-Cost Bounded Reachability in MDPs
- Tom van Dijk. Oink: an Implementation and Evaluation of Modern Parity Game Solvers
- Balasubramanian A.R., Nathalie Bertrand and Nicolas Markey. Parameterized verification of synchronization in constrained reconfigurable broadcast networks
- Lina Marsso, Radu Mateescu and Wendelin Serwe. TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
- Gabriele Costa, David Basin, Chiara Bodei, Pierpaolo Degano and Letterio Galletta. From Natural Projection to Partial Model Checking and Back
- Kshitij Bansal, Eric Koskinen and Omer Tripp. Automatic Generation of Precise and Useful Commutativity Conditions
- Maximilian Paul Louis Haslbeck and Tobias Nipkow. Hoare Logics for Time Bounds
- Luca Bortolussi and Simone Silvetti. Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models
- Milan Ceska, Vojtech Havlena, Lukas Holik, Ondrej Lengal and Tomas Vojnar. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection
- Daniel Neider, P. Madhusudan, Pranav Garg, Shambwaditya Saha and Daejun Park. Invariant Synthesis for Incomplete Verification Engines
- Philipp J. Meyer, Javier Esparza and Hagen Völzer. Computing the concurrency threshold of sound free-choice workflow nets
- Bohua Zhan. Efficient verification of imperative programs using auto2
- Radu Iosif and Xiao Xu. Abstraction Refinement for Emptiness Checking of Alternating Data Automata
- Peter Chini, Roland Meyer and Prakash Saivasan. Fine-Grained Complexity of Safety Verification
- Stefan Schupp and Erika Abraham. Efficient dynamic error reduction for hybrid systems reachability analysis
- Andrew Reynolds, Haniel Barbosa and Pascal Fontaine. Revisiting Enumerative Instantiation
- Daniel Hausmann, Lutz Schröder and Hans-Peter Deifel. Permutation Games for the Weakly Aconjunctive mu-Calculus
- Matthew Wicker, Xiaowei Huang and Marta Kwiatkowska. Feature-Guided Black-Box Safety Testing of Deep Neural Networks
- Kedar Namjoshi and Richard Trefler. Symmetry Reduction for the Local Mu-Calculus
- Quang Loc Le, Jun Sun and Shengchao Qin. Frame Inference for Inductive Entailment Proofs in Separation Logic
- Seonmo Kim and Stephen McCamant. Bit-Vector Model Counting using Statistical Estimation
- Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel and Michael Whalen. Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
- Rohit Dureja and Kristin Yvonne Rozier. More Scalable LTL Model Checking via Discovering Design-Space Dependencies
- Chuan Jiang and Gianfranco Ciardo. Generation of Minimum Tree-like Witnesses for Existential CTL
- Elena Sherman and Matthew Dwyer. Structurally Defined Conditional Data-flow Static Analysis
- Grigory Fedyukovich and Rastislav Bodik. Accelerating Syntax-Guided Invariant Synthesis
- Pierre Roux, Mohamed Iguernlala and Sylvain Conchon. An Non-linear Arithmetic Procedure for Control-Command Software Verification.
- Alexander J. Summers and Peter Müller. Automating Deductive Verification for Weak-Memory Programs
- Simon Wimmer and Peter Lammich. Verified Model Checking of Timed Automata
- Raphaël Cauderlier and Mihaela Sighireanu. A Verified Implementation of the Bounded List Container
- Jan Leike and Matthias Heizmann. Geometric Nontermination Arguments
- Stavros Aronis, Bengt Jonsson, Magnus Lång and Konstantinos Sagonas. Optimal Dynamic Partial Order Reduction with Observers