TACAS 2021 programme

All times are in CEST (GMT+2)

Monday, March 29
10h40 - 12h00 TACAS

Game Theory/Model checking (Chair: Marcin Jurdzinski)

  • Benjamin Bisping, Uwe Nestmann. A Game for Linear-time–Branching-time Spectroscopy [doi]
  • Suguman Bansal, Krishnendu Chatterjee, Moshe Y. Vardi. On Satisficing in Quantitative Games [doi]
  • Daniel Hausmann, Lutz Schröder. Quasipolynomial Computation of Nested Fixpoints [doi]
  • Tzu-Han Hsu, César Sánchez, Borzoo Bonakdarpour. Bounded Model Checking for Hyperproperties [doi]
15h20 - 16h40

TACAS
SMT Verification (Chair: Joost-Pieter Katoen)

  • Seulkee Baek, Mario Carneiro, Marijn J. H. Heule. A Flexible Proof Format for SAT Solver-Elaborator Communication [doi]
  • Randal E. Bryant, Marijn J. H. Heule. Generating Extended Resolution Proofs with a BDD-Based SAT Solver [doi] (nominated for EATCS best paper award)
  • Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays [doi]
  • Muhammad Osama, Anton Wijs, Armin Biere. SAT Solving with GPU Accelerated Inprocessing [doi]

17h00 -

18:20 

 

TACAS 
Probabilities (Chair: David N. Jansen)

  • Jip Spel, Sebastian Junges, Joost-Pieter Katoen. Finding Provably Optimal Markov Chains [doi]
  • Roman Andriushchenko, Milan Češka, Sebastian Junges, Joost-Pieter Katoen. Inductive Synthesis for Probabilistic Programs Reaches New Horizons [doi]
  • Michael Backenköhler, Luca Bortolussi, Gerrit Großmann, Verena Wolf. Analysis of  Markov Jump Processes under Terminal Constraints [doi]
  • Tim Quatmann, Joost-Pieter Katoen. Multi-objective Optimization of Long-run Average and Total Rewards [doi]
Tuesday, March 30
10h40 - 12h00 TACAS

Timed systems (Chair: Susanne Graf)

  • Jaroslav Bendík, Ahmet Sencan, Ebru Aydin Gol, Ivana Černá. Timed Automata Relaxation for Reachability [doi]
  • Étienne André, Jaime Arias, Laure Petrucci, Jaco van de Pol. Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata [doi]
  • Konstantinos Mamouras, Agnishom Chattopadhyay, Zhifu Wang. Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring [doi]
  • Fabian Meyer, Marcel Hark, Jürgen Giesl. Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes [doi]
14h00 - 15h20

TACAS 
Neural networks (Chair: Armin Biere)

  • Daniel M. Yellin, Gail Weiss. Synthesizing Context-free Grammars from Recurrent Neural Networks [doi]
  • Andrea Peruffo, Daniele Ahmed, Alessandro Abate. Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [doi]
  • Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, Lijun Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement [doi]
  • Guy Amir, Haoze Wu, Clark Barrett, Guy Katz. An SMT-Based Approach for Verifying Binarized Neural Networks [doi]

17h00 -

18h20

TACAS 
Analysis of network communication (Chair: Hossein Hojjat)

  • Stefan Schmid, Nicolas Schnepf, Jiří Srba. Resilient Capacity-Aware Routing [doi]
  • Lei Shi, Yahui Li, Boon Thau Loo, Rajeev Alur. Network Traffic Classification by Program Synthesis [doi]
  • Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche. General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond [doi] (EAPLS best paper award winner)
  • Anjiang Wei, Pu Yi, Tao Xie, Darko Marinov, Wing Lam. Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests [doi]
Wednesday, March 31
10h40 - 12h00

TACAS

Verification techniques (not SMT) (Chair: Jan Strejcek)

  • Michael Blondin, Christoph Haase, Philip Offtermatt. Directed Reachability for Infinite-State Systems [doi]
  • Grigory Fedyukovich, Gidon Ernst. Bridging Arrays and ADTs in Recursive Proofs [doi]
  • Margarida Ferreira, Miguel Terra-Neves, Miguel Ventura, Inês Lynce, Ruben Martins. FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions [doi]
  • Nikola Beneš, Luboš Brim, Samuel Pastva, David Šafránek. Symbolic Coloured SCC Decomposition [doi]
14h00 - 15h20

TACAS
Case studies/floating point (Chair: Thierry Lecomte)

  • Aviad Cohen, Alexander Nadel, Vadim Ryvchin. Local Search with a SAT Oracle for Combinatorial Optimization [doi]
  • Julien Lepiller, Ruzica Piskac, Martin Schäf, Mark Santolucito. Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities [doi]
  • Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, Wolfgang Ahrendt. Deductive Verification of Floating-Point Java Programs in KeY [doi] (nominated for EAPLS best paper award)
  • Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis. A Two-Phase Approach for Conditional Floating-Point Verification [doi]
14h00 - 15h20

SV-Comp

Software Verification: 10th Comparative Evaluation (SV-COMP 2021) [doi]

  • Dirk Beyer. SV-COMP 2021 Report [doi]
  • Vadim Mutilin. CPA-BAM-BnB
  • Stephan Holzner. CPAchecker [doi]
  • Pavel Andrianov. CPALockator [doi]
  • Hernan Ponce de Leon. Dartagnan [doi]
  • Martin Spießl. Frama-C
  • Zsófia Ádám. Gazer-Theta [doi]
  • Simmo Saan. Goblint [doi]
  • Malte Mues. JDart [doi]
  • Soha Hussein. Java-Ranger
  • Ali Shamakhi. JayHorn [doi]
  • Gidon Ernst. Korn
  • Martin Spießl. MetaVal [doi]
  • Marek Chalupa. Symbiotic [doi]
  • Matthias Heizmann. Ultimate Automizer

15h40 -

17h00

TACAS 
Tools (verification) (Chair: Thomas Neele)

  • Daniela Kaufmann, Armin Biere. AMulet 2.0 for Verifying Multiplier Circuits of Rewriting [doi]
  • Manuel Gieseking, Jesko Hecking-Harbusch, Ann Yanich. A Web Interface for Petri Nets with Transits and Petri Games [doi]
  • Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, Atsushi Igarashi. Helmholtz: A Verifier for Tezos Smart [doi]
  • Maximilian A. Köhl, Michaela Klauck, Holger Hermanns. Momba: JANI Meets Python [doi]

15h40 -

17h00

SV-Comp

Open Community Meeting on Software Verification

Thursday, April 1
10h40 - 12h00

TACAS
Machine learning/SMT (Chair: Radu Mateescu)

  • Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen. cake_lpr: Verified Propagation Redundancy Checking in CakeML [doi]
  • Pranav Ashok, Mathias Jackermeier, Jan Křetínský, Christoph Weinhuber, Maximilian Weininger, Mayank Yadav. dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts [doi]
  • Matthew Sotoudeh, Aditya V. Thakur. SyReNN: A Tool for Analyzing Deep Neural Networks [doi]
  • Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh. MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers [doi]
15h20 - 16h40

TACAS
Proof generation/validation (Chair: Laura Kovács)

  • Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhaue. Certifying Proofs in the First-Order Theory [doi]
  • Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. Syntax-Guided Quantifier Instantiation [doi] (nominated for EATCS best paper award)
  • Giles Reger, Johannes Schoisswohl, Andrei Voronkov. Making Theory Reasoning Simpler [doi]
  • Yong Kiam Tan, André Platzer. Deductive Stability Proofs for Ordinary Differential Equations [doi]

17h00 -

18h00

TACAS 
Tools (testing and monitoring) (Chair: Frédéric Lang)

  • Felipe Gorostiaga, César Sánchez. HLola: a Very Functional Tool for Extensible Stream Runtime Verification [doi]
  • Carlos E. Budde, Arnd Hartmanns. Replicating Restart with Prolonged Retrials: An Experimental Report [doi]
  • Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, Maximilian A. Köhl, Yannik Schnitzer, Maximilian Schwenger. RTLola on Board: Testing Real Driving Emissions on Your Phone [doi] (nominated for EASST best paper award)

 

Who's online

We have 104 guests and no members online

Site Hosted by