TACAS 2021 Accepted Papers

Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue and Lijun Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement
Jaroslav Bendík, Ahmet Sencan, Ebru Aydin Gol and Ivana Černá. Timed Automata Relaxation for Reachability
Randal E. Bryant and Marijn J. H. Heule. Generating Extended Resolution Proofs with a BDD-Based SAT Solver
Michael Blondin, Christoph Haase and Philip Offtermatt. Directed Reachability for Infinite-State Systems
Guy Amir, Haoze Wu, Clark Barrett and Guy Katz. An SMT-Based Approach for Verifying Binarized Neural Networks
Yong Kiam Tan, Marijn Heule and Magnus O. Myreen. cake_lpr: Verified Propagation Redundancy Checking in CakeML
Tzu-Han Hsu, Cesar Sanchez and Borzoo Bonakdarpour. Bounded Model Checking for Hyperproperties
Felipe Gorostiaga and Cesar Sanchez. HLola: a Very Functional Tool for Extensible Stream Runtime Verification
Fabian Meyer, Marcel Hark and Jürgen Giesl. Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Étienne André, Jaime Arias, Laure Petrucci and Jaco van de Pol. Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon and Clark Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Daniela Kaufmann and Armin Biere. AMulet 2.0 for Verifying Multiplier Circuits
Aviad Cohen, Alexander Nadel and Vadim Ryvchin. Local Search with a SAT Oracle for Combinatorial Optimization
Michael Backenköhler, Luca Bortolussi, Gerrit Großmann and Verena Wolf. Analysis of Markov Jump Processes under Terminal Constraints
Benjamin Bisping and Uwe Nestmann. A Game for Linear-time–Branching-time Spectroscopy
Yong Kiam Tan and André Platzer. Deductive Stability Proofs for Ordinary Differential Equations
Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova and Maria Christakis. A Two-Phase Approach for Conditional Floating-Point Verification
Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich and Wolfgang Ahrendt. Deductive Verification of Floating-Point Java Programs in KeY
Yuki Nishida, Hiromasa Saito, Chen Ran, Akira Kawata, Jun Furuse, Kouhei Suenaga and Atsushi Igarashi. Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
Stefan Schmid, Nicolas Schnepf and Jiri Srba. Resilient Capacity-Aware Routing
Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian Köhl, Yannik Schnitzer and Maximilian Schwenger. RTLola on Board: Testing Real Driving Emissions on your Phone
Margarida Ferreira, Miguel Terra-Neves, Miguel Ventura, Inês Lynce and Ruben Martins. FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions
Carlos E. Budde and Arnd Hartmanns. Replicating Restart with Prolonged Retrials: An Experimental Report
Andrea Peruffo, Daniele Ahmed and Alessandro Abate. Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
Giles Reger, Johannes Schoisswohl and Andrei Voronkov. Making Theory Reasoning Simpler
Nikola Benes, Lubos Brim, Samuel Pastva and David Šafránek. Symbolic Coloured SCC Decomposition
Seulkee Baek, Mario Carneiro and Marijn Heule. A Flexible Proof Format for SAT Solver-Elaborator Communication
Matthew Sotoudeh and Aditya Thakur. SyReNN: A Tool for Analyzing Deep Neural Networks
Suguman Bansal, Krishnendu Chatterjee and Moshe Vardi. On Satisficing in Quantitative Games
Roman Andriushchenko, Milan Ceska, Sebastian Junges and Joost-Pieter Katoen. Inductive Synthesis for Probabilistic Programs Reaches New Horizons
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati and Vijay Ganesh. MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
Konstantinos Mamouras, Agnishom Chattopadhyay and Zhifu Wang. Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring
Tim Quatmann and Joost-Pieter Katoen. Multi-objective Optimization of Long-run Average and Total Rewards
Grigory Fedyukovich and Gidon Ernst. Bridging Arrays and ADTs in Recursive Proofs
Julien Lepiller, Ruzica Piskac, Martin Schaef and Mark Santolucito. Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. Syntax-Guided Quantifier Instantiation
Lei Shi, Yahui Li, Boon Thau Loo and Rajeev Alur. Network Traffic Classification by Program Synthesis
Anjiang Wei, Pu Yi, Tao Xie, Darko Marinov and Wing Lam. Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests
Daniel Yellin and Gail Weiss. Synthesizing Context-free Grammars from Recurrent Neural Networks
Manuel Gieseking, Jesko Hecking-Harbusch and Ann Yanich. A Web Interface for Petri Nets with Transits and Petri Games
Muhammad Osama, Anton Wijs and Armin Biere. SAT Solving with GPU Accelerated Inprocessing
Rupak Majumdar, Ramanathan Thinniyam Srinivasan and Georg Zetzsche. General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
Alexander Lochmann, Fabian Mitterwallner, Aart Middeldorp and Bertram Felgenhauer. Certifying Proofs in the First-Order Theory of Rewriting
Jip Spel, Sebastian Junges and Joost-Pieter Katoen. Finding Provably Optimal Markov Chains
Pranav Ashok, Mathias Jackermeier, Jan Kretinsky, Christoph Weinhuber, Maximilian Weininger and Mayank Yadav. dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts
Daniel Hausmann and Lutz Schröder. Quasipolynomial Computation of Nested Fixpoints

Who's online

We have 66 guests and no members online

Site Hosted by